Derivatives for Containers in Univalent Foundations
Cubical.HITs.SetTruncation
Initializing search
    phijor/derivatives
    • Overview
    • Library
    phijor/derivatives
    • Overview
      • Derivative.Bag
      • Derivative.Adjunction
      • Derivative.Basics.Sum
      • Derivative.Basics.Unit
      • Derivative.Basics.W
      • Derivative.Basics.Decidable
      • Derivative.Basics.Embedding
      • Derivative.Basics.Equiv
      • Derivative.Basics.Maybe
      • Derivative.Basics.Sigma
      • Derivative.Category
      • Derivative.ChainRule
      • Derivative.Container
      • Derivative.Derivative
      • Derivative.Indexed.Mu
      • Derivative.Indexed.ChainRule
      • Derivative.Indexed.Container
      • Derivative.Indexed.Derivative
      • Derivative.Indexed.MuRule
      • Derivative.Indexed.Univalence
      • Derivative.Isolated.Base
      • Derivative.Isolated
      • Derivative.Isolated.S1
      • Derivative.Isolated.Sum
      • Derivative.Isolated.W
      • Derivative.Isolated.DependentGrafting
      • Derivative.Isolated.Grafting
      • Derivative.Isolated.Maybe
      • Derivative.Isolated.Sigma
      • Derivative.Prelude
      • Derivative.Properties
      • Derivative.Remove

    Cubical.HITs.SetTruncation

    module Cubical.HITs.SetTruncation where

open import Cubical.HITs.SetTruncation.Base public
open import Cubical.HITs.SetTruncation.Properties public
    Made with Material for MkDocs