Library HoTT.Contrib.HoTTBook
Library HoTT.Contrib.HoTTBookExercises
Library HoTT.Contrib.SetoidRewrite
Library HoTT.Contrib.UniverseLevel
Library HoTT.Tests.Algebra.Groups.Presentation
Library HoTT.Tests.Classes.ring_tac
Library HoTT.Tests.Idempotents
Library HoTT.Tests.Metatheory.FunextVarieties
Library HoTT.Tests.Metatheory.UnivalenceImpliesFunext
Library HoTT.Tests.Pointed.Core
Library HoTT.Tests.WildCat.Opposite
Library HoTT.Tests.bugs.github1358
Library HoTT.Tests.bugs.github1382
Library HoTT.Tests.bugs.github1758
Library HoTT.Tests.bugs.github1759
Library HoTT.Tests.bugs.github1791
Library HoTT.Tests.bugs.github1794
Library HoTT.Tests.bugs.github370
Library HoTT.Tests.bugs.github390
Library HoTT.Tests.bugs.github726
Library HoTT.Tests.bugs.github754
Library HoTT.Tests.bugs.github973
Library HoTT.Algebra.AbGroups
Library HoTT.Algebra.AbGroups.AbHom
Library HoTT.Algebra.AbGroups.AbProjective
Library HoTT.Algebra.AbGroups.AbPullback
Library HoTT.Algebra.AbGroups.AbPushout
Library HoTT.Algebra.AbGroups.AbelianGroup
Library HoTT.Algebra.AbGroups.Abelianization
Library HoTT.Algebra.AbGroups.Biproduct
Library HoTT.Algebra.AbGroups.Centralizer
Library HoTT.Algebra.AbGroups.Cyclic
Library HoTT.Algebra.AbGroups.Z
Library HoTT.Algebra.AbSES
Library HoTT.Algebra.AbSES.BaerSum
Library HoTT.Algebra.AbSES.Core
Library HoTT.Algebra.AbSES.DirectSum
Library HoTT.Algebra.AbSES.Ext
Library HoTT.Algebra.AbSES.Pullback
- Pullbacks of short exact sequences
Library HoTT.Algebra.AbSES.PullbackFiberSequence
Library HoTT.Algebra.AbSES.Pushout
Library HoTT.Algebra.AbSES.SixTerm
Library HoTT.Algebra.Aut
Library HoTT.Algebra.Congruence
Library HoTT.Algebra.Groups
Library HoTT.Algebra.Groups.FreeGroup
Library HoTT.Algebra.Groups.FreeProduct
Library HoTT.Algebra.Groups.Group
- Groups
- Some basic properties of groups
- Group homomorphisms
- Basic properties of group homomorphisms
- Group Isomorphisms
- Simple group equivalences
- Reasoning with equations in groups.
- Cancelation lemmas
- Group movement lemmas
- Power operation
- The category of Groups
- Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms.
- The trivial group
- The direct product of groups
- Free groups
- Further properties of group homomorphisms.
Library HoTT.Algebra.Groups.GroupCoeq
Library HoTT.Algebra.Groups.GrpPullback
Library HoTT.Algebra.Groups.Image
Library HoTT.Algebra.Groups.Kernel
Library HoTT.Algebra.Groups.Lagrange
Library HoTT.Algebra.Groups.Presentation
Library HoTT.Algebra.Groups.QuotientGroup
Library HoTT.Algebra.Groups.ShortExactSequence
Library HoTT.Algebra.Groups.Subgroup
Library HoTT.Algebra.Rings
Library HoTT.Algebra.Rings.CRing
Library HoTT.Algebra.Rings.ChineseRemainder
Library HoTT.Algebra.Rings.Ideal
Library HoTT.Algebra.Rings.Module
Library HoTT.Algebra.Rings.QuotientRing
Library HoTT.Algebra.Rings.Ring
Library HoTT.Algebra.Rings.Z
Library HoTT.Algebra.Universal.Algebra
Library HoTT.Algebra.Universal.Congruence
Library HoTT.Algebra.Universal.Homomorphism
Library HoTT.Algebra.Universal.Operation
Library HoTT.Algebra.Universal.TermAlgebra
Library HoTT.Algebra.ooAction
Library HoTT.Algebra.ooGroup
Library HoTT.Analysis.Locator
Library HoTT.Axioms.Funext
Library HoTT.Axioms.Univalence
Library HoTT.Basics
Library HoTT.Basics.Contractible
Library HoTT.Basics.Datatypes
Library HoTT.Basics.Decidable
Library HoTT.Basics.Decimal
Library HoTT.Basics.Equivalences
Library HoTT.Basics.Hexadecimal
Library HoTT.Basics.Logic
Library HoTT.Basics.Nat
Library HoTT.Basics.Notations
Library HoTT.Basics.Numeral
Library HoTT.Basics.Overture
- Basic definitions of homotopy type theory, particularly the groupoid structure of identity types.
- That's not technically true; it might be possible to get non-parametric universe polymorphism using Modules and (Module) Functors; we can use functors to quantify over a Module Type which requires a polymorphic proof of a given hypothesis, and then use that hypothesis polymorphically in any theorem we prove in our new Module Functor. But that is far beyond the scope of this file.
Library HoTT.Basics.PathGroupoids
- The groupid structure of paths
Library HoTT.Basics.Tactics
Library HoTT.Basics.Trunc
Library HoTT.Basics.Utf8
Library HoTT.BoundedSearch
Library HoTT.Categories
- Category Theory
- Categories
- Functors
- Natural Transformations
- Functor Categories
- Groupoids
- Precategory of Groupoids
- Discrete Categories
- Indiscrete Categories
- Finite Discrete Categories (natural numbers as categories)
- Chain Categories [n]
- Initial and Terminal Categories
- The Category of Sets
- The Category of Simplicial Sets
- The Category of Semi-Simplicial Sets
- The Hom Functor
- Profunctors
- The Category of Categories
- Laws about Functor Categories
- Laws about Product Categories
- Comma Categories
- Universal Properties and Universal Morphisms
- Kan Extensions
- Adjunctions
- Limits
- Pseudofunctors
- Pseudonatural Transformations
- Lax Comma Categories
- Duality as a Functor
- The Grothendieck Construction
- The Category of Sections of a Functor
- The Dependent Product
- The Yoneda Lemma
- The Structure Identity Principle
- Fundamental Pregroupoids
- Homotopy PreCategory
Library HoTT.Categories.Adjoint
Library HoTT.Categories.Adjoint.Composition
Library HoTT.Categories.Adjoint.Composition.AssociativityLaw
Library HoTT.Categories.Adjoint.Composition.Core
Library HoTT.Categories.Adjoint.Composition.IdentityLaws
Library HoTT.Categories.Adjoint.Composition.LawsTactic
Library HoTT.Categories.Adjoint.Core
Library HoTT.Categories.Adjoint.Dual
Library HoTT.Categories.Adjoint.Functorial
Library HoTT.Categories.Adjoint.Functorial.Core
Library HoTT.Categories.Adjoint.Functorial.Laws
Library HoTT.Categories.Adjoint.Functorial.Parts
Library HoTT.Categories.Adjoint.Hom
Library HoTT.Categories.Adjoint.HomCoercions
Library HoTT.Categories.Adjoint.Identity
Library HoTT.Categories.Adjoint.Notations
Library HoTT.Categories.Adjoint.Paths
Library HoTT.Categories.Adjoint.Pointwise
Library HoTT.Categories.Adjoint.UnitCounit
Library HoTT.Categories.Adjoint.UnitCounitCoercions
Library HoTT.Categories.Adjoint.UniversalMorphisms
Library HoTT.Categories.Adjoint.UniversalMorphisms.Core
Library HoTT.Categories.Adjoint.Utf8
Library HoTT.Categories.Cat
Library HoTT.Categories.Cat.Core
Library HoTT.Categories.Cat.Morphisms
Library HoTT.Categories.Category
Library HoTT.Categories.Category.Core
Library HoTT.Categories.Category.Dual
Library HoTT.Categories.Category.Morphisms
- Definitions and theorems about {iso,epi,mono,}morphisms in a precategory
- Definition of isomorphism
- Theorems about isomorphisms
- The inverse of a morphism is unique
- Equivalence between the record and sigma versions of IsIsomorphism
- Being an isomorphism is a mere proposition
- Equivalence between record and sigma versions of Isomorphic
- Equivalence between record and fully sigma versions of Isomorphic
- Isomorphisms form an hSet
- Equality between isomorphisms is determined by equality between their forward components
- Relations between path_isomorphic, ap morphism_inverse, and ap morphism_isomorphic
- Equality between isomorphisms is equivalent to by equality between their forward components
- The identity is an isomorphism
- Inverses of isomorphisms are isomorphisms
- Composition of isomorphisms gives an isomorphism
- Being isomorphic is a reflexive relation
- Being isomorphic is a symmetric relation
- Being isomorphic is a transitive relation
- Equality gives rise to isomorphism
- Epimorphisms and Monomorphisms
- The identity is an epimorphism
- The identity is a monomorphism
- Composition of epimorphisms gives an epimorphism
- Composition of monomorphisms gives a monomorphism
- Existence of {epi,mono}morphisms are a preorder
- Retractions are epimorphisms
- Sections are monomorphisms
- Isomorphisms are both sections and retractions
- Isomorphisms are therefore epimorphisms and monomorphisms
- Lemmas about idtoiso
- Lemmas about how to move isomorphisms around equalities, following HoTT.PathGroupoids
- Tactics for moving inverses around
- Tactics for collapsing p ∘ p⁻¹ and p⁻¹ ∘ p
Library HoTT.Categories.Category.Notations
Library HoTT.Categories.Category.Objects
Library HoTT.Categories.Category.Paths
- Classification of path spaces of precategories
- Classify sufficient conditions to prove precategories equal
- Equality of precategorys gives rise to an inhabitant of the path-classifying-type
- Classify equality of precategorys up to equivalence
- Curried version of path classifying lemma
- Curried version of path classifying lemma, using ∀ in place of equality of functions
- Tactic for proving equality of precategories
Library HoTT.Categories.Category.Pi
Library HoTT.Categories.Category.Prod
Library HoTT.Categories.Category.Sigma
Library HoTT.Categories.Category.Sigma.Core
Library HoTT.Categories.Category.Sigma.OnMorphisms
Library HoTT.Categories.Category.Sigma.OnObjects
Library HoTT.Categories.Category.Sigma.Univalent
Library HoTT.Categories.Category.Strict
Library HoTT.Categories.Category.Subcategory
Library HoTT.Categories.Category.Subcategory.Full
Library HoTT.Categories.Category.Subcategory.Wide
Library HoTT.Categories.Category.Sum
Library HoTT.Categories.Category.Univalent
Library HoTT.Categories.Category.Utf8
Library HoTT.Categories.CategoryOfGroupoids
Library HoTT.Categories.CategoryOfSections
Library HoTT.Categories.CategoryOfSections.Core
Library HoTT.Categories.ChainCategory
Library HoTT.Categories.Comma
Library HoTT.Categories.Comma.Core
Library HoTT.Categories.Comma.Dual
Library HoTT.Categories.Comma.Functorial
Library HoTT.Categories.Comma.InducedFunctors
Library HoTT.Categories.Comma.Notations
Library HoTT.Categories.Comma.Projection
Library HoTT.Categories.Comma.ProjectionFunctors
Library HoTT.Categories.Comma.Utf8
Library HoTT.Categories.DependentProduct
Library HoTT.Categories.DiscreteCategory
Library HoTT.Categories.DualFunctor
Library HoTT.Categories.ExponentialLaws
Library HoTT.Categories.ExponentialLaws.Law0
Library HoTT.Categories.ExponentialLaws.Law1
Library HoTT.Categories.ExponentialLaws.Law1.Functors
Library HoTT.Categories.ExponentialLaws.Law1.Law
Library HoTT.Categories.ExponentialLaws.Law2
Library HoTT.Categories.ExponentialLaws.Law2.Functors
Library HoTT.Categories.ExponentialLaws.Law2.Law
Library HoTT.Categories.ExponentialLaws.Law3
Library HoTT.Categories.ExponentialLaws.Law3.Functors
Library HoTT.Categories.ExponentialLaws.Law3.Law
Library HoTT.Categories.ExponentialLaws.Law4
Library HoTT.Categories.ExponentialLaws.Law4.Functors
Library HoTT.Categories.ExponentialLaws.Law4.Law
Library HoTT.Categories.ExponentialLaws.Tactics
Library HoTT.Categories.Functor
Library HoTT.Categories.Functor.Attributes
Library HoTT.Categories.Functor.Composition
Library HoTT.Categories.Functor.Composition.Core
Library HoTT.Categories.Functor.Composition.Functorial
Library HoTT.Categories.Functor.Composition.Functorial.Attributes
Library HoTT.Categories.Functor.Composition.Functorial.Core
Library HoTT.Categories.Functor.Composition.Laws
Library HoTT.Categories.Functor.Core
Library HoTT.Categories.Functor.Dual
Library HoTT.Categories.Functor.Identity
Library HoTT.Categories.Functor.Notations
Library HoTT.Categories.Functor.Paths
- Classification of path spaces of functors
- Equivalence between the record and sigma-type versions of a functor
- Classify sufficient conditions to prove functors equal
- Equality of functors gives rise to an inhabitant of the path-classifying-type
- Curried version of path classifying lemma
- Curried version of path classifying lemma, using ∀ in place of equality of functions
- Classify equality of functors up to equivalence
- If the objects in D are n-truncated, then so is the type of functors C → D
- Tactic for proving equality of functors
- Tactic for pushing ap object_of through other aps.
Library HoTT.Categories.Functor.Pointwise
Library HoTT.Categories.Functor.Pointwise.Core
Library HoTT.Categories.Functor.Pointwise.Properties
Library HoTT.Categories.Functor.Prod
Library HoTT.Categories.Functor.Prod.Core
Library HoTT.Categories.Functor.Prod.Functorial
Library HoTT.Categories.Functor.Prod.Universal
Library HoTT.Categories.Functor.Sum
Library HoTT.Categories.Functor.Utf8
Library HoTT.Categories.FunctorCategory
Library HoTT.Categories.FunctorCategory.Core
Library HoTT.Categories.FunctorCategory.Dual
Library HoTT.Categories.FunctorCategory.Functorial
Library HoTT.Categories.FunctorCategory.Morphisms
Library HoTT.Categories.FunctorCategory.Notations
Library HoTT.Categories.FunctorCategory.Utf8
Library HoTT.Categories.FundamentalPreGroupoidCategory
Library HoTT.Categories.Grothendieck
Library HoTT.Categories.Grothendieck.PseudofunctorToCat
Library HoTT.Categories.Grothendieck.ToCat
Library HoTT.Categories.Grothendieck.ToSet
Library HoTT.Categories.Grothendieck.ToSet.Core
Library HoTT.Categories.Grothendieck.ToSet.Morphisms
Library HoTT.Categories.Grothendieck.ToSet.Univalent
Library HoTT.Categories.GroupoidCategory
Library HoTT.Categories.GroupoidCategory.Core
Library HoTT.Categories.GroupoidCategory.Dual
Library HoTT.Categories.GroupoidCategory.Morphisms
Library HoTT.Categories.HomFunctor
Library HoTT.Categories.HomotopyPreCategory
Library HoTT.Categories.IndiscreteCategory
Library HoTT.Categories.InitialTerminalCategory
Library HoTT.Categories.InitialTerminalCategory.Core
Library HoTT.Categories.InitialTerminalCategory.Functors
Library HoTT.Categories.InitialTerminalCategory.NaturalTransformations
Library HoTT.Categories.InitialTerminalCategory.Notations
Library HoTT.Categories.InitialTerminalCategory.Pseudofunctors
Library HoTT.Categories.KanExtensions
Library HoTT.Categories.KanExtensions.Core
Library HoTT.Categories.KanExtensions.Functors
Library HoTT.Categories.LaxComma
Library HoTT.Categories.LaxComma.Core
Library HoTT.Categories.LaxComma.CoreLaws
Library HoTT.Categories.LaxComma.CoreParts
Library HoTT.Categories.LaxComma.Notations
Library HoTT.Categories.LaxComma.Utf8
Library HoTT.Categories.Limits
Library HoTT.Categories.Limits.Core
Library HoTT.Categories.Limits.Functors
Library HoTT.Categories.Monoidal.MonoidalCategory
Library HoTT.Categories.NatCategory
Library HoTT.Categories.NaturalTransformation
- Natural Transformations
- Definition of natural transformation
- Composition of natural transformations
- Dual natural transformations
- Identity natural transformation
- Natural isomorphisms
- Path space of natural transformation type
- Pointwise natural transformations
- Sums of natural transformations
- Products of natural transformations
Library HoTT.Categories.NaturalTransformation.Composition
Library HoTT.Categories.NaturalTransformation.Composition.Core
Library HoTT.Categories.NaturalTransformation.Composition.Functorial
Library HoTT.Categories.NaturalTransformation.Composition.Laws
- Laws about composition of functors
- left identity : 1 ∘ T = T
- right identity : T ∘ 1 = T
- right whisker left identity : 1 ∘ᴿ F = 1
- left whisker right identity : G ∘ᴸ 1 = 1
- whisker exchange law : (G' ∘ᴸ T) ∘ (T' ∘ᴿ F) = (T' ∘ᴿ F') ∘ (G ∘ᴸ T)
- left whisker composition : F ∘ᴸ (T ∘ T') = (F ∘ᴸ T) ∘ (F ∘ᴸ T')
- right whisker composition : (T ∘ T') ∘ᴿ F = (T ∘ᴿ F) ∘ (T' ∘ᴿ F)
- associators - natural transformations between F ∘ (G ∘ H) and (F ∘ G) ∘ H
- associativity : (T ∘ U) ∘ V = T ∘ (U ∘ V)
- left unitors : natural transformations between 1 ∘ F and F
- right unitors : natural transformations between F ∘ 1 and F
- Tactics for inserting appropriate associators, whiskers, and unitors
Library HoTT.Categories.NaturalTransformation.Core
Library HoTT.Categories.NaturalTransformation.Dual
Library HoTT.Categories.NaturalTransformation.Identity
Library HoTT.Categories.NaturalTransformation.Isomorphisms
- Natural isomorphisms
- Natural isomorphism respects composition
- Left whiskering preserves natural isomorphisms
- Right whiskering preserves natural isomorphisms
- action of idtoiso on objects
- idtoiso respsects composition
- left whiskering respects idtoiso
- right whiskering respects idtoiso
- Equalities induced by isomorphisms of objects
Library HoTT.Categories.NaturalTransformation.Notations
Library HoTT.Categories.NaturalTransformation.Paths
- Classify the path space of natural transformations
- Equivalence between record and sigma versions of natural transformation
- The type of natural transformations is an hSet
- Equality of natural transformations is implied by equality of components
- Equality of natural transformations is equivalent to equality of components
- Tactic for proving equality of natural transformations
Library HoTT.Categories.NaturalTransformation.Pointwise
Library HoTT.Categories.NaturalTransformation.Prod
Library HoTT.Categories.NaturalTransformation.Sum
Library HoTT.Categories.NaturalTransformation.Utf8
Library HoTT.Categories.Notations
Library HoTT.Categories.ProductLaws
Library HoTT.Categories.Profunctor
Library HoTT.Categories.Profunctor.Core
Library HoTT.Categories.Profunctor.Identity
Library HoTT.Categories.Profunctor.Notations
Library HoTT.Categories.Profunctor.Representable
Library HoTT.Categories.Profunctor.Utf8
Library HoTT.Categories.Pseudofunctor
Library HoTT.Categories.Pseudofunctor.Core
Library HoTT.Categories.Pseudofunctor.FromFunctor
Library HoTT.Categories.Pseudofunctor.Identity
Library HoTT.Categories.Pseudofunctor.RewriteLaws
Library HoTT.Categories.PseudonaturalTransformation
Library HoTT.Categories.PseudonaturalTransformation.Core
Library HoTT.Categories.SemiSimplicialSets
Library HoTT.Categories.SetCategory
Library HoTT.Categories.SetCategory.Core
Library HoTT.Categories.SetCategory.Functors
Library HoTT.Categories.SetCategory.Functors.SetProp
Library HoTT.Categories.SetCategory.Morphisms
Library HoTT.Categories.SimplicialSets
Library HoTT.Categories.Structure
Library HoTT.Categories.Structure.Core
Library HoTT.Categories.Structure.IdentityPrinciple
Library HoTT.Categories.Structure.Notations
Library HoTT.Categories.Structure.Utf8
Library HoTT.Categories.UniversalProperties
Library HoTT.Categories.Utf8
Library HoTT.Categories.Yoneda
Library HoTT.Classes.categories.ua_category
Library HoTT.Classes.implementations.assume_rationals
Library HoTT.Classes.implementations.binary_naturals
Library HoTT.Classes.implementations.bool
Library HoTT.Classes.implementations.family_prod
Library HoTT.Classes.implementations.field_of_fractions
Library HoTT.Classes.implementations.hprop_lattice
Library HoTT.Classes.implementations.natpair_integers
Library HoTT.Classes.implementations.ne_list
Library HoTT.Classes.implementations.peano_naturals
Library HoTT.Classes.implementations.pointwise
Library HoTT.Classes.interfaces.abstract_algebra
Library HoTT.Classes.interfaces.archimedean
Library HoTT.Classes.interfaces.canonical_names
Library HoTT.Classes.interfaces.cauchy
Library HoTT.Classes.interfaces.integers
Library HoTT.Classes.interfaces.monad
Library HoTT.Classes.interfaces.naturals
Library HoTT.Classes.interfaces.orders
Library HoTT.Classes.interfaces.rationals
Library HoTT.Classes.interfaces.round
Library HoTT.Classes.interfaces.ua_algebra
Library HoTT.Classes.interfaces.ua_congruence
Library HoTT.Classes.interfaces.ua_setalgebra
Library HoTT.Classes.isomorphisms.rings
Library HoTT.Classes.orders.archimedean
Library HoTT.Classes.orders.dec_fields
Library HoTT.Classes.orders.fields
Library HoTT.Classes.orders.integers
Library HoTT.Classes.orders.lattices
Library HoTT.Classes.orders.maps
Library HoTT.Classes.orders.nat_int
Library HoTT.Classes.orders.naturals
Library HoTT.Classes.orders.orders
Library HoTT.Classes.orders.rings
Library HoTT.Classes.orders.semirings
Library HoTT.Classes.orders.sum
Library HoTT.Classes.tactics.ring_pol
Library HoTT.Classes.tactics.ring_quote
Library HoTT.Classes.tactics.ring_tac
Library HoTT.Classes.theory.additional_operations
Library HoTT.Classes.theory.apartness
Library HoTT.Classes.theory.dec_fields
Library HoTT.Classes.theory.fields
Library HoTT.Classes.theory.groups
Library HoTT.Classes.theory.int_abs
Library HoTT.Classes.theory.integers
Library HoTT.Classes.theory.lattices
Library HoTT.Classes.theory.nat_distance
Library HoTT.Classes.theory.naturals
Library HoTT.Classes.theory.premetric
Library HoTT.Classes.theory.rationals
Library HoTT.Classes.theory.rings
Library HoTT.Classes.theory.ua_first_isomorphism
Library HoTT.Classes.theory.ua_homomorphism
Library HoTT.Classes.theory.ua_isomorphic
Library HoTT.Classes.theory.ua_prod_algebra
Library HoTT.Classes.theory.ua_quotient_algebra
Library HoTT.Classes.theory.ua_second_isomorphism
Library HoTT.Classes.theory.ua_subalgebra
Library HoTT.Classes.theory.ua_third_isomorphism
Library HoTT.Colimits.Coeq
Library HoTT.Colimits.CoeqUnivProp
Library HoTT.Colimits.Colimit
- Colimits
- Existence of colimits
- Functoriality of colimits
- Unicity of colimits
- Colimits are left adjoint to constant diagram
Library HoTT.Colimits.Colimit_Coequalizer
Library HoTT.Colimits.Colimit_Flattening
Library HoTT.Colimits.Colimit_Prod
Library HoTT.Colimits.Colimit_Pushout
Library HoTT.Colimits.Colimit_Pushout_Flattening
Library HoTT.Colimits.Colimit_Sigma
Library HoTT.Colimits.GraphQuotient
Library HoTT.Colimits.MappingCylinder
Library HoTT.Colimits.Pushout
Library HoTT.Colimits.Quotient
Library HoTT.Colimits.Quotient.Choice
Library HoTT.Colimits.Sequential
Library HoTT.Colimits.SpanPushout
Library HoTT.Constant
Library HoTT.Cubical
Library HoTT.Cubical.DPath
Library HoTT.Cubical.DPathCube
Library HoTT.Cubical.DPathSquare
Library HoTT.Cubical.PathCube
Library HoTT.Cubical.PathSquare
Library HoTT.DProp
Library HoTT.Diagrams.Cocone
Library HoTT.Diagrams.CommutativeSquares
Library HoTT.Diagrams.Cone
Library HoTT.Diagrams.ConstantDiagram
Library HoTT.Diagrams.DDiagram
Library HoTT.Diagrams.Diagram
Library HoTT.Diagrams.Graph
Library HoTT.Diagrams.ParallelPair
Library HoTT.Diagrams.Sequence
Library HoTT.Diagrams.Span
Library HoTT.Equiv.BiInv
Library HoTT.Equiv.PathSplit
Library HoTT.Equiv.Relational
Library HoTT.EquivGroupoids
Library HoTT.ExcludedMiddle
Library HoTT.Extensions
Library HoTT.Factorization
Library HoTT.Functorish
Library HoTT.HFiber
Library HoTT.HIT.Flattening
Library HoTT.HIT.FreeIntQuotient
Library HoTT.HIT.Interval
Library HoTT.HIT.SetCone
Library HoTT.HIT.V
- The cumulative hierarchy V.
- The cumulative hierarchy V
- Alternative induction principle (This is close to the one from the book)
- Membership relation
- Subset relation
- Bisimulation relation
- Canonical presentation of V-sets (Lemma 10.5.6)
- Lemmas 10.5.8 (i) & (vii), we put them here because they are useful later
- Two useful lemmas
- Definitions of particular sets in V
- Axioms of set theory (theorem 10.5.8)
Library HoTT.HIT.epi
Library HoTT.HIT.iso
Library HoTT.HIT.quotient
Library HoTT.HIT.surjective_factor
Library HoTT.HIT.unique_choice
Library HoTT.HProp
Library HoTT.HSet
Library HoTT.HoTT
Library HoTT.Homotopy.BlakersMassey
Library HoTT.Homotopy.Bouquet
Library HoTT.Homotopy.CayleyDickson
Library HoTT.Homotopy.ClassifyingSpace
Library HoTT.Homotopy.Cover
Library HoTT.Homotopy.EMSpace
Library HoTT.Homotopy.EncodeDecode
Library HoTT.Homotopy.EvaluationFibration
Library HoTT.Homotopy.ExactSequence
Library HoTT.Homotopy.Freudenthal
Library HoTT.Homotopy.HSpace
Library HoTT.Homotopy.HSpace.Coherent
Library HoTT.Homotopy.HSpace.Core
Library HoTT.Homotopy.HSpace.Moduli
Library HoTT.Homotopy.HSpace.Pointwise
Library HoTT.Homotopy.HSpaceS1
Library HoTT.Homotopy.HomotopyGroup
Library HoTT.Homotopy.Hopf
Library HoTT.Homotopy.Join
Library HoTT.Homotopy.Join.Core
- Joins
- Join_rec gives an equivalence of 0-groupoids
- Various types of equalities between paths in joins
- Functoriality of Join.
- Symmetry of Join
- Other miscellaneous results about joins
Library HoTT.Homotopy.Join.JoinAssoc
Library HoTT.Homotopy.Join.JoinSusp
Library HoTT.Homotopy.Join.TriJoin
- Induction and recursion principles for the triple join
- ap_trijoin and ap_trijoin_transport
- The induction principle for the triple join
- The recursion principle for the triple join, and many results about it
- The graph structure on TriJoinRecData A B C P
- trijoin_rec_inv is an injective map between 0-groupoids
- Lemmas and tactics about triangles and prisms
- Use the WildCat library to organize things
- trijoinrecdata_0gpd A B C is a 1-functor from Type to ZeroGpd
- Functoriality of the triple join
Library HoTT.Homotopy.PinSn
Library HoTT.Homotopy.Smash
Library HoTT.Homotopy.SuccessorStructure
Library HoTT.Homotopy.Suspension
Library HoTT.Homotopy.Syllepsis
Library HoTT.Homotopy.Wedge
Library HoTT.Homotopy.WhiteheadsPrinciple
Library HoTT.Idempotents
Library HoTT.Limits.Equalizer
Library HoTT.Limits.Limit
- Limits
- Existence of limits
- Functoriality of limits
- Unicity of limits
- Limits are right adjoint to constant diagram
Library HoTT.Limits.Pullback
Library HoTT.Metatheory.Core
Library HoTT.Metatheory.FunextVarieties
Library HoTT.Metatheory.IntervalImpliesFunext
Library HoTT.Metatheory.PropTrunc
Library HoTT.Metatheory.TruncImpliesFunext
Library HoTT.Metatheory.UnivalenceImpliesFunext
Library HoTT.Metatheory.UnivalenceVarieties
Library HoTT.Misc
Library HoTT.Modalities.Accessible
Library HoTT.Modalities.Closed
Library HoTT.Modalities.CoreflectiveSubuniverse
Library HoTT.Modalities.Descent
Library HoTT.Modalities.Fracture
Library HoTT.Modalities.Identity
Library HoTT.Modalities.Lex
Library HoTT.Modalities.Localization
Library HoTT.Modalities.Meet
Library HoTT.Modalities.Modality
Library HoTT.Modalities.Notnot
Library HoTT.Modalities.Nullification
Library HoTT.Modalities.Open
Library HoTT.Modalities.ReflectiveSubuniverse
- Reflective Subuniverses
- References
- Definitions
- Properties of Subuniverses
- Properties of Reflective Subuniverses
- The Unit type
- Dependent product and arrows
- Product
- Pullbacks
- Fibers
- Equivalences
- Paths
- Truncations
- Coproducts
- Coequalizers
- Pushouts
- Modally connected types
- Modally truncated maps
- Modally connected maps
- Containment of (reflective) subuniverses
- Equality of (reflective) subuniverses
- Separated subuniverses
Library HoTT.Modalities.Separated
Library HoTT.Modalities.Topological
Library HoTT.NullHomotopy
Library HoTT.ObjectClassifier
Library HoTT.PathAny
Library HoTT.Pointed
Library HoTT.Pointed.Core
- Pointed Types
- Pointed functions
- Pointed homotopies
- Pointed equivalences
- Equivalences to sigma-types.
- Various operations with pointed homotopies
- Whiskering of pointed homotopies by pointed functions
- 1-categorical properties of pType.
- 1-categorical properties of pForall.
- The pointed category structure of pType
- pType and pForall as wild categories
- Pointed categories give rise to pointed structures
Library HoTT.Pointed.Loops
Library HoTT.Pointed.pEquiv
Library HoTT.Pointed.pFiber
Library HoTT.Pointed.pMap
Library HoTT.Pointed.pModality
Library HoTT.Pointed.pSect
Library HoTT.Pointed.pSusp
Library HoTT.Pointed.pTrunc
Library HoTT.Projective
Library HoTT.PropResizing.ImpredicativeTruncation
Library HoTT.PropResizing.Nat
Library HoTT.PropResizing.PropResizing
Library HoTT.Sets.AC
Library HoTT.Sets.GCH
Library HoTT.Sets.GCHtoAC
- Constructive equivalences
- Equivalences relying on LEM
- Equivalences on infinite sets
- Variants of Cantors's theorem
- Sierpinski's Theorem
Library HoTT.Sets.Hartogs
Library HoTT.Sets.Ordinals
- Well-foundedness
- Extensionality
- Ordinals
- Paths in Ordinal
- Simulations
- Initial segments
- `Ordinal` is an ordinal
- Ordinal successor
- Ordinal limit
Library HoTT.Sets.Powers
Library HoTT.Spaces.BAut
Library HoTT.Spaces.BAut.Bool
Library HoTT.Spaces.BAut.Bool.IncoherentIdempotent
Library HoTT.Spaces.BAut.Cantor
Library HoTT.Spaces.BAut.Rigid
Library HoTT.Spaces.Cantor
Library HoTT.Spaces.Card
Library HoTT.Spaces.Circle
Library HoTT.Spaces.Finite
Library HoTT.Spaces.Finite.Fin
Library HoTT.Spaces.Finite.FinInduction
Library HoTT.Spaces.Finite.FinNat
Library HoTT.Spaces.Finite.FinSeq
Library HoTT.Spaces.Finite.Finite
- Definition of general finite sets
- Preservation of finiteness by equivalences
- Simple examples of finite sets
- Decidability
- Induction over finite sets
- The finite axiom of choice, and projectivity
- Constructions on finite sets
- Finite sums of natural numbers
- Finite products of natural numbers
- Finite subsets
- Quotients
- Injections
- Surjections
- Enumerations
Library HoTT.Spaces.Finite.Tactics
Library HoTT.Spaces.Int
Library HoTT.Spaces.Int.Core
Library HoTT.Spaces.Int.Equiv
Library HoTT.Spaces.Int.LoopExp
Library HoTT.Spaces.Int.Spec
- Addition is commutative
- Zero is the additive identity.
- Multiplication by zero is zero
- One is the multiplicative identity
- Inverse laws
- Permutation of neg and pos_succ
- Permutation of pos and pos_succ
- Negation of a doubled positive integer
- int_succ is a retract of int_pred
- int_pred is a retract of int_succ
- Negation distributes over addition
- Negation is injective
- Subtracting 1 from a sucessor gives the positive integer.
- Subtracting a sucessor from 1 gives minus the integer.
- Interaction of doubling functions and subtraction
- Subtractions cancel sucessors.
- Predecessor of a subtraction is the subtraction of a sucessor.
- Negation of the predecessor is an involution.
- Predecessor of a sum is the sum with a predecessor
- Subtraction from a sum is the sum of a subtraction
- Associativity of addition
- Relationship between int_succ, int_pred and addition.
- Commutativity of multiplication
Library HoTT.Spaces.List.Core
Library HoTT.Spaces.List.Paths
Library HoTT.Spaces.List.Theory
Library HoTT.Spaces.Nat
Library HoTT.Spaces.Nat.Arithmetic
Library HoTT.Spaces.Nat.Core
- Theorems about the natural numbers
- Basic operations on naturals
- Minimum, maximum
- Power
- Euclidean division
- Greatest common divisor
- Square
- Square root
- Log2
- Equality of natural numbers
- Inequality of natural numbers
- Arithmetic
- Exponentiation
- Factorials
- Natural number ordering
- Theorems about natural number ordering
- Arithmetic relations between trunc_index and nat.
Library HoTT.Spaces.Nat.Paths
Library HoTT.Spaces.No
Library HoTT.Spaces.No.Addition
Library HoTT.Spaces.No.Core
- The surreal numbers
Library HoTT.Spaces.No.Negation
Library HoTT.Spaces.Pos
Library HoTT.Spaces.Pos.Core
- Binary Positive Integers
- Positive binary integers have decidable paths
- Operations over positive numbers
- Addition
- Operation x → 2*x-1
- Predecessor
- An auxiliary type for subtraction
- Operation x → 2*x+1
- Operation x → 2*x
- Operation x → 2*x-2
- Predecessor with mask
- Subtraction, result as a mask
- Subtraction, result as a positive, returning 1 if x≤y
- Multiplication
- Iteration over a positive number
- Iteration of a two-variable function, with nesting reflecting the bits
- Power
- Square
- Division by 2 rounded below but for 1
- Number of digits in a positive number
- From binary positive numbers to Peano natural numbers
- From Peano natural numbers to binary positive numbers
- Conversion with a decimal representation for printing/parsing
Library HoTT.Spaces.Pos.Spec
Library HoTT.Spaces.Spheres
Library HoTT.Spaces.Torus.Torus
Library HoTT.Spaces.Torus.TorusEquivCircles
Library HoTT.Spaces.Torus.TorusHomotopy
Library HoTT.Spaces.TwoSphere
Library HoTT.Spaces.Universe
Library HoTT.Spectra.Spectrum
Library HoTT.Tactics
Library HoTT.Tactics.BinderApply
Library HoTT.Tactics.EquivalenceInduction
Library HoTT.Tactics.EvalIn
Library HoTT.Tactics.Nameless
- Building blocks for a globally nameless style of tactic reasoning
- hyp returns any hypothesis, with subsequent failures backtracking through all hypotheses
- enforce foo ensures that foo is well-typed
- syntax_enforce [ H := body ] ensures that H has a body which is syntactically equal to body
- enforce [ x = y ] ensures that two terms, possibly containing holes, are judgmentally equal
Library HoTT.Tactics.RewriteModuloAssociativity
Library HoTT.TruncType
Library HoTT.Truncations
Library HoTT.Truncations.Connectedness
Library HoTT.Truncations.Core
Library HoTT.Truncations.SeparatedTrunc
Library HoTT.Types
Library HoTT.Types.Arrow
Library HoTT.Types.Bool
Library HoTT.Types.Empty
Library HoTT.Types.Equiv
Library HoTT.Types.Forall
- Theorems about dependent products
- Paths
- Path algebra
- Transport
- Maps on paths
- Dependent paths
- Functorial action
- Equivalences
- Functoriality on logical equivalences
- Two variable versions for function extensionality.
- Truncatedness: any dependent product of n-types is an n-type: see contr_forall and istrunc_forall in Basics.Trunc.
- Contractibility: A product over a contractible type is equivalent to the fiber over the center.
- Symmetry of curried arguments
Library HoTT.Types.IWType
- Reduction of indexed W-types to W-types
- M. Abbott, T. Altenkirch, and N. Ghani. Containers - constructing strictly positive types. Theoretical Computer Science, 342:327, September 2005. Applied Semantics: Selected Topics.
- N. Gambino and M. Hyland. Wellfounded trees and dependent polynomial functors. In S. Berardi, M. Coppo, and F. Damiani, editors, types for Proofs and Programs (TYPES 2003), Lecture Notes in Computer Science, 2004
- Characterization of path types of IW-types. Argument due to Jasper Hugunin.
Library HoTT.Types.Paths
Library HoTT.Types.Prod
Library HoTT.Types.Sigma
Library HoTT.Types.Sum
- Theorems about disjoint unions
- CoUnpacking
- Eta conversion
- Paths
- Fibers of inl and inr
- Decomposition
- Transport
- Detecting the summands
- Functorial action
- "Unfunctorial action"
- Functoriality on equivalences
- Unfunctoriality on equivalences
- Symmetry
- Associativity
- Identity
- Distributivity
- Extensivity
- Indecomposability
- Universal mapping properties
- Sums preserve most truncation
- Decidability
- Binary coproducts are equivalent to dependent sigmas where the first component is a bool.
Library HoTT.Types.Unit
Library HoTT.Types.Universe
Library HoTT.Types.WType
Library HoTT.Utf8
Library HoTT.Utf8Minimal
Library HoTT.WildCat
Library HoTT.WildCat.Adjoint
Library HoTT.WildCat.Bifunctor
Library HoTT.WildCat.Coproducts
Library HoTT.WildCat.Core
Library HoTT.WildCat.Displayed
Library HoTT.WildCat.DisplayedEquiv
Library HoTT.WildCat.EmptyCat
Library HoTT.WildCat.Equiv
- Equivalences in wild categories
- Initial objects and terminal objects are all respectively equivalent.
- There is a default notion of equivalence for a 1-category, namely bi-invertibility.
Library HoTT.WildCat.EquivGpd
Library HoTT.WildCat.Forall
Library HoTT.WildCat.FunctorCat
Library HoTT.WildCat.Induced
Library HoTT.WildCat.Monoidal
- Monoidal Categories
Library HoTT.WildCat.NatTrans
Library HoTT.WildCat.Opposite
Library HoTT.WildCat.Paths
Library HoTT.WildCat.PointedCat
Library HoTT.WildCat.Prod
Library HoTT.WildCat.Products
Library HoTT.WildCat.Sigma
Library HoTT.WildCat.Square
Library HoTT.WildCat.Sum
Library HoTT.WildCat.TwoOneCat
Library HoTT.WildCat.UnitCat
Library HoTT.WildCat.Universe
Library HoTT.WildCat.Yoneda
Library HoTT.WildCat.ZeroGroupoid
This page has been generated by coqdoc