Library HoTT.Contrib.HoTTBook

Library HoTT.Contrib.HoTTBookExercises

Library HoTT.Contrib.SetoidRewrite

Library HoTT.Contrib.UniverseLevel

• Universe Levels

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

• Homomorphisms from a group to an abelian group form an abelian group.
  • The bifunctor ab_hom
  • Properties of ab_hom

Library HoTT.Algebra.AbGroups.AbProjective

• Projective abelian groups

Library HoTT.Algebra.AbGroups.AbPullback

• Pullbacks of abelian groups

Library HoTT.Algebra.AbGroups.AbPushout

• Pushouts of abelian groups.
  • Properties of pushouts of maps

Library HoTT.Algebra.AbGroups.AbelianGroup

• Abelian groups
  • Paths between abelian groups
  • Subgroups of abelian groups
  • Quotients of abelian groups
  • The wild category of abelian groups
  • Kernels of abelian groups
  • Transporting in families related to abelian groups
  • Operations on abelian groups

Library HoTT.Algebra.AbGroups.Abelianization

Library HoTT.Algebra.AbGroups.Biproduct

• Biproducts of abelian groups
  • • Functoriality of ab_biprod
    • Lemmas for working with biproducts

Library HoTT.Algebra.AbGroups.Centralizer

Library HoTT.Algebra.AbGroups.Cyclic

• Cyclic groups
  • The free group on one generator
• Finite cyclic groups

Library HoTT.Algebra.AbGroups.Z

• The group of integers

Library HoTT.Algebra.AbSES

Library HoTT.Algebra.AbSES.BaerSum

• The Baer sum of two short exact sequences, lemmas and consequences.
  • AbSES' is a bifunctor
  • Pushouts and pullbacks respect the Baer sum

Library HoTT.Algebra.AbSES.Core

• Short exact sequences of abelian groups
  • Paths in AbSES B A
    • The wildcat of short exact sequences
    • Path data lemmas
    • Homotopies of path data
    • Characterisation of loops of short exact sequences
  • Morphisms of short exact sequences
  • Characterization of split short exact sequences
  • Constructions of short exact sequences

Library HoTT.Algebra.AbSES.DirectSum

• The direct sum of short exact sequences

Library HoTT.Algebra.AbSES.Ext

• The set Ext B A of abelian group extensions
  • The bifunctor ab_ext
  • Extensions ending in a projective are trivial

Library HoTT.Algebra.AbSES.Pullback

• Pullbacks of short exact sequences
  • The universal property of abses_pullback_morphism
  • Functoriality of abses_pullback f for f : B' $-> B
  • Functoriality of abses_pullback
    • Pulling back along constant maps
    • Pulling E back along projection E is trivial
    • Pulling back along homotopic maps
    • Pulling back along a complex
    • Fibers of pullback in terms of path data
    • AbSES and AbSES' become contravariant functors in the first variable by pulling back

Library HoTT.Algebra.AbSES.PullbackFiberSequence

• The fiber sequence induced by pulling back along a short exact sequence

Library HoTT.Algebra.AbSES.Pushout

• Pushouts of short exact sequences
  • The universal property of abses_pushout_morphism
  • Functoriality of abses_pushout f : AbSES B A → AbSES B A'
  • Functoriality of pushing out

Library HoTT.Algebra.AbSES.SixTerm

• The contravariant six-term sequence of Ext
  • • Exactness of ab_hom E G → ab_hom A G → Ext B G
    • Exactness of ab_hom A G → Ext1 B G → Ext1 E G.
    • Exactness of Ext B G → Ext E G → Ext A G
    • Ext Z/n A is isomorphic to A/n

Library HoTT.Algebra.Aut

• Automorphism oo-Groups

Library HoTT.Algebra.Congruence

Library HoTT.Algebra.Groups

Library HoTT.Algebra.Groups.FreeGroup

• • Subgroups of free groups

Library HoTT.Algebra.Groups.FreeProduct

Library HoTT.Algebra.Groups.Group

• Groups
  • Definition of a Group
  • Proof automation
• 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
    • Moving group elements
    • Moving inverses.
    • Moving elements equal to unit.
    • Cancelling elements equal to unit.
  • 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
    • Properties of maps to and from the trivial group
  • 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

• Kernels of group homomorphisms
  • Corecursion principle for group kernels
  • Characterisation of group embeddings

Library HoTT.Algebra.Groups.Lagrange

• • Lagrange's theorem

Library HoTT.Algebra.Groups.Presentation

• • Fundamental theorem of presentations of groups
  • Constructors for finite presentations
  • Notations for presentations

Library HoTT.Algebra.Groups.QuotientGroup

• Quotient groups

Library HoTT.Algebra.Groups.ShortExactSequence

• Complexes of groups

Library HoTT.Algebra.Groups.Subgroup

• Subgroups
  • • The subgroup generated by a subset

Library HoTT.Algebra.Rings

Library HoTT.Algebra.Rings.CRing

• Commutative Rings
  • Properties of commutative rings
  • Ideals in commutative rings
  • Category of commutative rings.

Library HoTT.Algebra.Rings.ChineseRemainder

• Chinese remainder theorem

Library HoTT.Algebra.Rings.Ideal

• Left, Right and Two-sided Ideals
  • Definition of Ideals
    • Truncatedness properties
    • Conversion between Ideals
    • Easy properties of ideals
  • Constructions of ideals
    • Zero Ideal
    • The unit ideal
    • Intersection of ideals
    • Sum of ideals
    • Product of ideals
    • The kernel of a ring homomorphism
    • Ideal generated by a subset
    • Finitely gnerated ideal.
    • Principal ideals
    • Ideal equality
    • Subset relation on ideals
    • Quotient (a.k.a colon) ideals
    • Annihilator
  • Properties of ideals
    • Coprime ideals
    • Ideal notations
    • Ideal lemmas

Library HoTT.Algebra.Rings.Module

• Left modules over a ring.
  • Definition
  • Facts about left modules
  • Left Submodules
  • Left R-module homomorphisms
  • Category of left R-modules
  • Kernel of module homomorphism
  • Image of module homomorphism
  • Quotient Modules
  • First Isomorphism Theorem
  • Direct products

Library HoTT.Algebra.Rings.QuotientRing

• Quotient Rings
  • • Specialized induction principles
  • Quotient thoery

Library HoTT.Algebra.Rings.Ring

• Rings
  • Ring laws
  • Ring movement lemmas
  • Wild category of rings
  • Product ring
  • Image ring
    • More Ring laws

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

• Actions of oo-Groups

Library HoTT.Algebra.ooGroup

• oo-Groups
  • Definition
  • Homomorphisms
    • Definition
    • Functoriality
    • Homomorphic properties
  • Subgroups
  • 1-groups as oo-groups

Library HoTT.Analysis.Locator

Library HoTT.Axioms.Funext

Library HoTT.Axioms.Univalence

Library HoTT.Basics

Library HoTT.Basics.Contractible

• Contractibility

Library HoTT.Basics.Datatypes

Library HoTT.Basics.Decidable

• Decidability
  • Definitions
  • Decidable hprops
  • Transfer along equivalences
  • Hedberg's theorem: any type with decidable equality is a set.
  • Truncation

Library HoTT.Basics.Decimal

• Decimal numbers

Library HoTT.Basics.Equivalences

• Equivalences
  • Building equivalences between nested sigma and record types

Library HoTT.Basics.Hexadecimal

• Hexadecimal numbers

Library HoTT.Basics.Logic

Library HoTT.Basics.Nat

• • Tail-recursive versions of add and mul
  • Conversion with a decimal representation for printing/parsing

Library HoTT.Basics.Notations

• • Notation scopes

Library HoTT.Basics.Numeral

• Decimal or Hexadecimal numbers

Library HoTT.Basics.Overture

• Basic definitions of homotopy type theory, particularly the groupoid structure of identity types.
  • Type classes
  • Basic definitions
    • Constant functions
  • Sigma types
  • The groupoid structure of identity types.
  • Equivalences
  • Applying paths between equivalences like functions
  • Contractibility and truncation levels
    • Contractibility and truncation levels
    • Truncated relations
    • Function extensionality
• 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.
  • • Tactics
  • Natural numbers
    • Pointed types
    • Homotopy fibers
    • More tactics

Library HoTT.Basics.PathGroupoids

• The groupid structure of paths
  • Naming conventions
  • The 1-dimensional groupoid structure.
    • Theorems for moving things around in equations.
    • Functoriality of functions
    • Action of apD10 and ap10 on paths.
    • Transport and the groupoid structure of paths
  • ap11
    • ap for curried two variable functions
    • Transporting in particular fibrations.
    • The behavior of ap and apD.
  • The 2-dimensional groupoid structure
    • Whiskering
    • Unwhiskering, a.k.a. cancelling.
  • Tactics, hints, and aliases

Library HoTT.Basics.Tactics

• Basic tactics

Library HoTT.Basics.Trunc

• Truncatedness
  • Arithmetic on truncation-levels.
  • Truncatedness proper.
  • Truncated morphisms
  • Universes of truncated types
  • Facts about hprops
  • Truncatedness: any dependent product of n-types is an n-type

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

• Adjunctions
  • Definitions
    • unit+UMP
    • counit+UMP
    • unit+counit+zig+zag
    • universal morphisms
    • hom-set isomorphism
  • Coercions between various definitions
  • Opposite adjunctions
  • Path spaces of adjunctions
  • Composition
  • Pointwise adjunctions
  • Functoriality of any adjoint construction

Library HoTT.Categories.Adjoint.Composition

• Adjunction composition
  • Definition
  • Associativity
• Left and right identity laws

Library HoTT.Categories.Adjoint.Composition.AssociativityLaw

• Associativity of adjunction composition

Library HoTT.Categories.Adjoint.Composition.Core

• Composition of adjunctions F' ⊣ G' → F ⊣ G → (F' ∘ F) ⊣ (G ∘ G')
  • via the unit+counit+zig+zag definition

Library HoTT.Categories.Adjoint.Composition.IdentityLaws

• Left and right identity laws of adjunction composition

Library HoTT.Categories.Adjoint.Composition.LawsTactic

• Tactic for proving laws about adjoint composition

Library HoTT.Categories.Adjoint.Core

• Adjunctions

Library HoTT.Categories.Adjoint.Dual

• Opposite adjunction F ⊣ G → Gᵒᵖ ⊣ Fᵒᵖ
  • Definition of Aᵒᵖ
  • ᵒᵖ is judgmentally involutive

Library HoTT.Categories.Adjoint.Functorial

• Functoriality of the construction of adjunctions
  • Computational components
  • Functor laws
  • Adjunction functor

Library HoTT.Categories.Adjoint.Functorial.Core

• Functoriality of the construction of adjunctions
  • Non-dependent functor for left adjoints
  • Non-dependent functor for right adjoints

Library HoTT.Categories.Adjoint.Functorial.Laws

• Functoriality of the construction of adjunctions

Library HoTT.Categories.Adjoint.Functorial.Parts

• Functoriality of the construction of adjunctions from universal morphisms
  • action on morphisms of the construction of a left adjoint to G
    • functoriality on C, D, and G
    • functoriality in G
  • action on morphisms of the construction of a right adjoint to F

Library HoTT.Categories.Adjoint.Hom

• Hom-Set Adjunctions

Library HoTT.Categories.Adjoint.HomCoercions

• Coercions between hom-set adjunctions and unit+counit adjunctions
  • unit+UMP from hom-set adjunction
  • hom-set adjunction from unit+ump adjunction

Library HoTT.Categories.Adjoint.Identity

• Identity adjunction 1 ⊣ 1

Library HoTT.Categories.Adjoint.Notations

Library HoTT.Categories.Adjoint.Paths

• Classify the path space of adjunctions
  • Equivalence between record and nested sigma for unit+counit adjunctions
  • Adjunctions are an hSet
  • Equality of adjunctions follows from equality of unit+counit
  • Equality of adjunctions follows from equality of action of unit+counit on objects

Library HoTT.Categories.Adjoint.Pointwise

• Pointwise Adjunctions
  • F ⊣ G → E^F ⊣ E^G
  • F ⊣ G → Gᴱ ⊣ Fᴱ

Library HoTT.Categories.Adjoint.UnitCounit

• Adjunctions by units and counits
  • Unit + UMP definition of adjunction
  • Counit + UMP definition of adjunction
  • Unit + Counit + Zig + Zag definition of adjunction

Library HoTT.Categories.Adjoint.UnitCounitCoercions

• Coercions between the various (co)unit definitions
  • unit+counit+zig+zag → unit+UMP
  • unit+counit+zig+zag → counit+UMP
  • unit+UMP → unit+counit+zig+zag
  • counit+UMP → unit+counit+zig+zag

Library HoTT.Categories.Adjoint.UniversalMorphisms

• Adjunctions as universal morphisms
  • Definitions

Library HoTT.Categories.Adjoint.UniversalMorphisms.Core

• Adjunctions as universal morphisms
  • F ⊣ G gives an initial object of (Y / G) for all Y : C
  • F ⊣ G gives a terminal object of (F / X) for all X : D
  • an initial object of (Y / G) for all Y : C gives a left adjoint to G
  • a terminal object of (F / X) for all X : D gives a right adjoint to F

Library HoTT.Categories.Adjoint.Utf8

Library HoTT.Categories.Cat

• Cat, precategories of precategories
  • Definitions
  • Morphisms in cat

Library HoTT.Categories.Cat.Core

• Cat, the precategory of strict categories
  • The initial and terminal categories are initial and terminal objects in cat

Library HoTT.Categories.Cat.Morphisms

• Morphisms in cat
  • Lemmas relationship between transporting the action of functors on objects, and idtoiso

Library HoTT.Categories.Category

• Categories
  • Definition of precategories
  • Opposite precategories
  • Morphisms in precategories
  • Classification of path space
  • Universal objects
  • Product precategories
  • Dependent product precategories
  • ∑-precategories
  • Strict categories
  • Coproduct precategories
  • Categories (univalent or saturated)
  • Subcategories

Library HoTT.Categories.Category.Core

• Definition of a PreCategory
  • Simple laws about the identity morphism

Library HoTT.Categories.Category.Dual

• Opposite Category
  • Definition of Cᵒᵖ
  • ᵒᵖ is judgmentally involutive
  • Initial objects are opposite terminal objects, and vice versa

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
    • transporting across an equality of morphisms is the same as conjugating with idtoiso
    • idtoiso respects inverse
    • idtoiso respects composition
    • idtoiso respects application of functors on morphisms and objects
    • Functors preserve isomorphisms
  • 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

• Notations for categories

Library HoTT.Categories.Category.Objects

• Universal objects
  • Definition of "unique up to unique isomorphism"
  • Terminal objects
  • Initial objects
  • Initial and terminal objects are unique up to unique isomorphism

Library HoTT.Categories.Category.Paths

• Classification of path spaces of precategories
  • Classify sufficient conditions to prove precategories equal
    • Said proof respects object
    • Said proof respects idpath
  • 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

• Dependent Product Category
  • Definition of ∀, or ∏, for categories
  • The product of strict categories is strict

Library HoTT.Categories.Category.Prod

• Product Category
  • Definition of × for categories
  • The product of strict categories is strict

Library HoTT.Categories.Category.Sigma

• ∑-precategories

Library HoTT.Categories.Category.Sigma.Core

• ∑-categories - exploded Grothendieck constructions, or generalizations of subcategories
  • Definition of a sig-precategory
  • First projection functor
  • Variant of sig'-precategory when we are taking a subset of morphisms
    • Definition of sig-precategory
    • First projection functor

Library HoTT.Categories.Category.Sigma.OnMorphisms

• ∑-categories on morphisms - a category with the same objects, but a ∑ type for morphisms
  • Definition of sig_mor-precategory
  • First projection functor
  • Definition of sig_mor-precategory
  • First projection functor

Library HoTT.Categories.Category.Sigma.OnObjects

• ∑-categories on objects - a generalization of subcategories
  • Definition of sig_obj-precategory
  • First projection functor

Library HoTT.Categories.Category.Sigma.Univalent

• Lifting saturation from categories to sigma/subcategories
  • Lift saturation to sigma on objects whenever the property is an hProp
  • Lift saturation to sigma on objects whenever the property is automatically and uniquely true of isomorphisms
  • Lift saturation to sigma on both objects and morphisms

Library HoTT.Categories.Category.Strict

• Definition of a strict category

Library HoTT.Categories.Category.Subcategory

• Subcategories
  • Full
  • Wide

Library HoTT.Categories.Category.Subcategory.Full

• Full Subcategories

Library HoTT.Categories.Category.Subcategory.Wide

• Wide subcategories

Library HoTT.Categories.Category.Sum

• The coproduct of categories
  • Definition of + for categories

Library HoTT.Categories.Category.Univalent

• Definition of a univalent/saturated precategory, or just "category"
  • • The objects of a category are a 1-type

Library HoTT.Categories.Category.Utf8

• Unicode notations for categories

Library HoTT.Categories.CategoryOfGroupoids

• Groupoid, the precategory of strict groupoid categories

Library HoTT.Categories.CategoryOfSections

• Category of sections of a functor

Library HoTT.Categories.CategoryOfSections.Core

• Category of sections
  • Section of a functor
  • Definition of category of sections of a functor

Library HoTT.Categories.ChainCategory

• The category ω of (ℕ, ≤), and the chain categories [n]
  • Definitions
    • [ω], the linear order on ℕ
    • [n], a linear order on a finite set with n + 1 elements

Library HoTT.Categories.Comma

• Comma Categories
  • Definitions
  • Duals
  • Projection functors
  • Functoriality

Library HoTT.Categories.Comma.Core

• Comma categories
  • Comma category (S / T)
  • (co)slice category (a / F), (F / a)
  • (co)slice category over (a / C), (C / a)
  • category of arrows

Library HoTT.Categories.Comma.Dual

• Opposite comma categories
  • The dual functors (S / T) ↔ ((Tᵒᵖ / Sᵒᵖ)ᵒᵖ)

Library HoTT.Categories.Comma.Functorial

• Functoriality of the comma category construction

Library HoTT.Categories.Comma.InducedFunctors

• Induced functors between comma categories
  • Morphisms in (A → C)ᵒᵖ × (B → C) from (s₀, s₁) to (d₀, d₁) induce functors (s₀ / s₁) → (d₀ / d₁)
  • Morphisms in C from a to a' induce functors (C / a) → (C / a')
  • Functors A → A' functors (cat / A) → (cat / A')

Library HoTT.Categories.Comma.Notations

• Notations for comma categories

Library HoTT.Categories.Comma.Projection

• Projection functors from comma categories
  • First projection (S / T) → A × B (for S : A → C ← B : T)
  • First projections (S / a) → A and (a / S) → A

Library HoTT.Categories.Comma.ProjectionFunctors

• Functoriality of the comma category construction with projection functors
  • Functor from (A → C)ᵒᵖ × (B → C) to cat / (A × B)
  • Functor (C → D)ᵒᵖ → D → (cat / C)
  • Functor (C → D) → Dᵒᵖ → (cat / C)

Library HoTT.Categories.Comma.Utf8

• Unicode notations for comma categories

Library HoTT.Categories.DependentProduct

• Dependent Product; oplax limit of a functor to Cat

Library HoTT.Categories.DiscreteCategory

• Discrete category

Library HoTT.Categories.DualFunctor

• The functor ᵒᵖ : cat → cat

Library HoTT.Categories.ExponentialLaws

• Exponential Laws
  • Laws about the initial category
    • x⁰ ≅ 1
    • 0ˣ ≅ 0 if x ≠ 0
  • Laws about the terminal category
    • x¹ ≅ x
    • 1ˣ ≅ 1
  • The law that a sum in an exponent is a product
    • yⁿ⁺ᵐ ≅ yⁿ × yᵐ
  • The law that exponentiation distributes over product
    • (y × z)ⁿ ≅ yⁿ × zⁿ
  • Currying
    • (yⁿ)ᵐ ≅ yⁿᵐ

Library HoTT.Categories.ExponentialLaws.Law0

• Exponential laws about the initial category
  • x⁰ ≅ 1
  • 0ˣ ≅ 0 if x ≠ 0
  • 0⁰ ≅ 1

Library HoTT.Categories.ExponentialLaws.Law1

• Laws about the terminal category
  • x¹ ≅ x
  • 1ˣ ≅ 1

Library HoTT.Categories.ExponentialLaws.Law1.Functors

• Functors involving functor categories involving the terminal category
  • C¹ → C
  • C → C¹
  • 1ˣ → 1
  • 1 → 1ˣ
  • 1ˣ ≅ 1

Library HoTT.Categories.ExponentialLaws.Law1.Law

• Exponential laws about the terminal category
  • C¹ ≅ C

Library HoTT.Categories.ExponentialLaws.Law2

• The law that a sum in an exponent is a product
  • yⁿ⁺ᵐ ≅ yⁿ × yᵐ

Library HoTT.Categories.ExponentialLaws.Law2.Functors

• Exponential functors between products and sums in exponents
  • yⁿ⁺ᵐ → yⁿ × yᵐ
  • yⁿ × yᵐ → yⁿ⁺ᵐ

Library HoTT.Categories.ExponentialLaws.Law2.Law

• Exponential laws about products and sums in exponents
  • yⁿ⁺ᵐ ≅ yⁿ × yᵐ

Library HoTT.Categories.ExponentialLaws.Law3

• The law that exponentiation distributes over product
  • (y × z)ⁿ ≅ yⁿ × zⁿ

Library HoTT.Categories.ExponentialLaws.Law3.Functors

• Functors between an exponential of a product and a product of exponentials
  • (y × z)ⁿ → yⁿ × zⁿ
  • yⁿ × zⁿ → (y × z)ⁿ

Library HoTT.Categories.ExponentialLaws.Law3.Law

• Laws about an exponential of a product and a product of exponentials
  • (y × z)ⁿ ≅ yⁿ × zⁿ

Library HoTT.Categories.ExponentialLaws.Law4

• Currying
  • (yⁿ)ᵐ ≅ yⁿᵐ

Library HoTT.Categories.ExponentialLaws.Law4.Functors

• Functors about currying, between C₁ × C₂ → D and C₁ → (C₂ → D)
  • (yⁿ)ᵐ → yⁿᵐ
  • yⁿᵐ → (yⁿ)ᵐ

Library HoTT.Categories.ExponentialLaws.Law4.Law

• Law about currying
  • (C₁ × C₂ → D) ≅ (C₁ → (C₂ → D))

Library HoTT.Categories.ExponentialLaws.Tactics

• Miscellaneous helper tactics for proving exponential laws

Library HoTT.Categories.Functor

• Functors
  • Definition
  • Composition
  • Duals
  • Identity
  • Classification of path space
  • Product functors
  • Coproduct functors
  • Full, Faithful, Fully Faithful
  • Pointwise functors (functoriality of functor category construction)

Library HoTT.Categories.Functor.Attributes

• Attributes of functors (full, faithful, split essentially surjective)
  • Natural transformation hom_C(─, ─) → hom_D(Fᵒᵖ(─), F(─))
  • Full
  • Faithful
  • Fully Faithful
  • Fully Faithful → Full
  • Fully Faithful → Faithful
  • Full * Faithful → Fully Faithful
  • Split Essentially Surjective
  • Essentially Surjective
  • Weak Equivalence

Library HoTT.Categories.Functor.Composition

• Composition of functors
  • Definition of composition
  • Functoriality of composition
  • Laws about functor composition

Library HoTT.Categories.Functor.Composition.Core

• Composition of functors

Library HoTT.Categories.Functor.Composition.Functorial

Library HoTT.Categories.Functor.Composition.Functorial.Attributes

• Attributes of Functoriality of functor composition
  • Precomposition with an essentially surjective functor is faithful

Library HoTT.Categories.Functor.Composition.Functorial.Core

• Functoriality of functor composition

Library HoTT.Categories.Functor.Composition.Laws

• Laws about composition of functors
  • left identity : 1 ∘ F = F
  • right identity : F ∘ 1 = F
  • Action of left and right identity laws on objects
  • associativity : (H ∘ G) ∘ F = H ∘ (G ∘ F)
  • Action of associativity on objects
  • coherence triangle
  • coherence pentagon

Library HoTT.Categories.Functor.Core

• Definition of a functor

Library HoTT.Categories.Functor.Dual

• Opposite functors
  • Definition of Fᵒᵖ
  • ᵒᵖ is judgmentally involutive

Library HoTT.Categories.Functor.Identity

• Identity functor

Library HoTT.Categories.Functor.Notations

• Notations for functors

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
    • Said proof respects object_of
    • Said proof respects idpath
  • 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

• Pointwise functors (functoriality of the functor category construction)

Library HoTT.Categories.Functor.Pointwise.Core

• Functors between functor categories constructed pointwise
  • Construction of pointwise : (C → D) → (C' → D') from C' → C and D → D'
  • Construction of (C → D) → (C → D') from D → D'
  • Construction of (C → D) → (C' → D) from C' → C

Library HoTT.Categories.Functor.Pointwise.Properties

• Properties of pointwise functors
  • respects identity
  • respects composition

Library HoTT.Categories.Functor.Prod

• Functors involving product categories, and their properties
  • Definitions of various functors
  • Universal property
  • Functoriality

Library HoTT.Categories.Functor.Prod.Core

• Functors involving product categories
  • First and second projections from a product precategory
  • Product of two functors from the same domain
  • Pairing of two functors
  • Partially applied functors out of a product precategory

Library HoTT.Categories.Functor.Prod.Functorial

• Functoriality of product of functors
  • Construction of product of functors as a functor - _×_ : (C → D) × (C → D') → (C → D × D')

Library HoTT.Categories.Functor.Prod.Universal

• Universal properties of product categories
  • fst ∘ (a × b) = a
  • snd ∘ (a × b) = b
  • Universal property characterizing unique product of functors
  • Classification of path space of functors to a product precategory

Library HoTT.Categories.Functor.Sum

• Functors involving coproduct categories
  • Injections inl : C → C + D and inr : D → C + D
  • Coproduct of functors F + F' : C + C' → D
  • swap : C + D → D + C

Library HoTT.Categories.Functor.Utf8

• Unicode notations for functors

Library HoTT.Categories.FunctorCategory

• Functor category
  • Definition
  • Morphisms in a functor category
  • Functoriality of (_ → _)
  • Opposite functor (C → D) → (Cᵒᵖ → Dᵒᵖ)ᵒᵖ

Library HoTT.Categories.FunctorCategory.Core

• Functor category D → C (also Cᴰ and [D, C])
  • Definition of C → D
  • C → D is a strict category if D is

Library HoTT.Categories.FunctorCategory.Dual

• Dual functor categories
  • Functors (C → D) ↔ (Cᵒᵖ → Dᵒᵖ)ᵒᵖ
  • The above functors are isomorphisms

Library HoTT.Categories.FunctorCategory.Functorial

• Functoriality of functor category construction
  • (_ → _) is a functor catᵒᵖ × cat → cat

Library HoTT.Categories.FunctorCategory.Morphisms

• Morphisms in a functor category
  • Natural Isomorphisms - isomorphisms in a functor category
  • If T is an isomorphism, then so is T x for any x
  • If T x is an isomorphism for all x, then so is T
  • Variant of idtoiso for natural transformations

Library HoTT.Categories.FunctorCategory.Notations

• Notations for functor categories

Library HoTT.Categories.FunctorCategory.Utf8

• Unicode notations for functor categories

Library HoTT.Categories.FundamentalPreGroupoidCategory

• Fundamental Pregroupoids
  • Categorification of the fundamental pregroupoid of a type

Library HoTT.Categories.Grothendieck

• Grothendieck Construction
  • of a functor to Set
  • of a pseudofunctor to Cat
  • of a functor to Cat

Library HoTT.Categories.Grothendieck.PseudofunctorToCat

• Grothendieck Construction of a pseudofunctor to Cat
  • Category of elements
  • First projection functor

Library HoTT.Categories.Grothendieck.ToCat

• Grothendieck Construction of a functor to Cat
  • Category of elements
  • First projection functor

Library HoTT.Categories.Grothendieck.ToSet

• Grothendieck Construction of a functor to Set
  • construction
  • classification of morphisms
  • preservation of saturation

Library HoTT.Categories.Grothendieck.ToSet.Core

• Grothendieck Construction of a functor to Set
  • Category of elements
  • First projection functor

Library HoTT.Categories.Grothendieck.ToSet.Morphisms

• Classification of morphisms of the Grothendieck Construction of a functor to Set

Library HoTT.Categories.Grothendieck.ToSet.Univalent

• Saturation of the Grothendieck Construction of a functor to Set

Library HoTT.Categories.GroupoidCategory

• Groupoids
  • Definition
  • Morphisms in a groupoid
  • Propositional self-duality

Library HoTT.Categories.GroupoidCategory.Core

• Groupoids
  • Definition of what it means to be a groupoid
  • Categorification of the groupoid of a 1-type
  • 0-types give rise to strict (groupoid) categories

Library HoTT.Categories.GroupoidCategory.Dual

• Propositional self-duality of groupoid categories

Library HoTT.Categories.GroupoidCategory.Morphisms

• Morphisms in a groupoid
  • All groupoids are categories

Library HoTT.Categories.HomFunctor

• Hom Functor
  • Definition of hom : Cᵒᵖ × C → Set as a functor
  • Covariant hom functor hom_C(A, ─) : C → set
  • Contravariant hom functor hom_C(─, A) : Cᵒᵖ → set

Library HoTT.Categories.HomotopyPreCategory

• Homotopy PreCategory of Types
  • The Homotopy PreCategory of Types

Library HoTT.Categories.IndiscreteCategory

• Indiscrete category
  • Definition of an indiscrete category
    • Indiscrete categories are strict categories
    • Indiscrete categories are (saturated/univalent) categories
  • Functors to an indiscrete category are given by their action on objects

Library HoTT.Categories.InitialTerminalCategory

• Initial and terminal categories
  • Definitions
  • Functors to and from initial and terminal categories
  • Natural transformations between functors from initial categories and to terminal categories
  • Pseudounctors from initial and terminal categories

Library HoTT.Categories.InitialTerminalCategory.Core

• Initial and terminal category definitions
  • Terminal categories
  • Initial categories
  • Default intitial (0) and terminal (1) precategories.

Library HoTT.Categories.InitialTerminalCategory.Functors

• Functors to and from initial and terminal categories
  • • Functor to any terminal category
    • Constant functor from any terminal category
    • Functor from any initial category
    • Uniqueness principles about initial and terminal categories and functors

Library HoTT.Categories.InitialTerminalCategory.NaturalTransformations

• Natural transformations between functors from initial categories and to terminal categories

Library HoTT.Categories.InitialTerminalCategory.Notations

• Initial and terminal category notations

Library HoTT.Categories.InitialTerminalCategory.Pseudofunctors

• Pseudofunctors from initial and terminal categories
  • Constant functor from any terminal category
    • Functor from any initial category

Library HoTT.Categories.KanExtensions

• Kan Extensions
  • Definitions
  • Kan Extensions assemble into functors

Library HoTT.Categories.KanExtensions.Core

• Kan Extensions
  • Idea
  • Definitions
  • Ordinary or weak Kan extensions
    • Global Kan extensions
    • Pullback-along functor
    • Left Kan extensions
    • Right Kan extensions

Library HoTT.Categories.KanExtensions.Functors

• Kan extensions assemble into functors
  • Left Kan extension functor
  • Right Kan extension functor

Library HoTT.Categories.LaxComma

• Lax Comma Categories
  • Definitions

Library HoTT.Categories.LaxComma.Core

• Lax Comma Category
  • Definition of Lax Comma Category
  • Definition of Lax (Co)Slice Category
  • Definition of Lax (Co)Slice Category Over
  • Definition of Lax (Co)Slice Arrow Category

Library HoTT.Categories.LaxComma.CoreLaws

Library HoTT.Categories.LaxComma.CoreParts

Library HoTT.Categories.LaxComma.Notations

• Notations for lax comma categories

Library HoTT.Categories.LaxComma.Utf8

• Unicode notations for comma categories

Library HoTT.Categories.Limits

• Limits and Colimits
  • Definitions
  • (co)limits assemble into functors
    • which are adjoints to Δ

Library HoTT.Categories.Limits.Core

• Limits and Colimits
  • The diagonal or "constant diagram" functor Δ
  • Definition of Limit
  • Definition of Colimit

Library HoTT.Categories.Limits.Functors

• (co)limits assemble into functors
  • Colimit functor, which is left adjoint to Δ
  • Limit functor, which is right adjoint to Δ

Library HoTT.Categories.Monoidal.MonoidalCategory

Library HoTT.Categories.NatCategory

• Discrete categories on n objects
  • Fin n types, or CardinalityRepresentative
  • Fin n is an hSet
  • Define the categories n

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

• Composition of natural transformations
  • Composition
  • Functoriality
  • Laws about composition

Library HoTT.Categories.NaturalTransformation.Composition.Core

• Composition of natural transformations
  • Vertical composition
  • Whiskering

Library HoTT.Categories.NaturalTransformation.Composition.Functorial

• Functoriality of composition of natural transformations
  • whiskering on the left is a functor
  • whiskering on the right is a functor

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

• Definition of natural transformation
  • Helper lemmas

Library HoTT.Categories.NaturalTransformation.Dual

• Opposite natural transformations
  • Definition of Tᵒᵖ
  • ᵒᵖ is judgmentally involutive

Library HoTT.Categories.NaturalTransformation.Identity

• Identity natural transformation

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

• Notations for natural transformations

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

• Pointwise Natural Transformations
  • Tˣ for a natural transformation T : F → G and a functor x : C → D
  • Fᵀ for a natural transformation T : F' → G' and a functor F : C → D

Library HoTT.Categories.NaturalTransformation.Prod

• Natural transformations involving product categories
  • Product of natural transformations
  • Natural transformations between partially applied functors

Library HoTT.Categories.NaturalTransformation.Sum

• Coproduct of natural transformations

Library HoTT.Categories.NaturalTransformation.Utf8

• Unicode notations for natural transformations

Library HoTT.Categories.Notations

• Notations for categories

Library HoTT.Categories.ProductLaws

• Laws about product categories
  • Swap functor C × D → D × C
  • A × (B × C) ≅ (A × B) × C
  • Laws about the initial category 0
    • C × 0 ≅ 0
    • 0 × C ≅ 0
  • Laws about the terminal category 1
    • C × 1 ≅ C
    • 1 × C ≅ C

Library HoTT.Categories.Profunctor

• Profunctors
  • Definition
  • Identity Profunctor
  • Representable Profunctors

Library HoTT.Categories.Profunctor.Core

• Profunctors

Library HoTT.Categories.Profunctor.Identity

• Identity profunctor

Library HoTT.Categories.Profunctor.Notations

• Notations for profunctors

Library HoTT.Categories.Profunctor.Representable

• Representable profunctors

Library HoTT.Categories.Profunctor.Utf8

• Unicode notations for profunctors

Library HoTT.Categories.Pseudofunctor

• Pseudofunctors
  • Definition
  • Helper lemmas for rewriting
  • Construction from a functor to cat
  • Identity pseudofunctor

Library HoTT.Categories.Pseudofunctor.Core

• Pseudofunctors

Library HoTT.Categories.Pseudofunctor.FromFunctor

• Functors to cat are pseudofunctors

Library HoTT.Categories.Pseudofunctor.Identity

• Identity pseudofunctor

Library HoTT.Categories.Pseudofunctor.RewriteLaws

• Pseudofunctor rewriting helper lemmas

Library HoTT.Categories.PseudonaturalTransformation

• Pseudonatural Transformations
  • Definition of pseudonatural transformations

Library HoTT.Categories.PseudonaturalTransformation.Core

• Definition of pseudonatural transformation

Library HoTT.Categories.SemiSimplicialSets

• The category of semisimplicial sets

Library HoTT.Categories.SetCategory

• Category of sets
  • Definitoins of set_cat and prop_cat
  • Morphisms in the category of sets
  • Functors to/from the category of sets

Library HoTT.Categories.SetCategory.Core

• PreCategories set_cat and prop_cat
  • Prop is a strict category

Library HoTT.Categories.SetCategory.Functors

• Functors between set_cat and prop_cat

Library HoTT.Categories.SetCategory.Functors.SetProp

• Functors between set_cat and prop_cat
  • Functors to prop_cat give rise to functors to set_cat
  • Functors from set_cat give rise to functors to prop_cat

Library HoTT.Categories.SetCategory.Morphisms

• Morphisms in set_cat
  • Isomorphisms in set_cat are eqivalent to equivalences.
  • Isomorphisms in prop_cat are eqivalent to equivalences.

Library HoTT.Categories.SimplicialSets

• The simplex category Δ, and the precategory of simplicial sets, Δᵒᵖ → set

Library HoTT.Categories.Structure

Library HoTT.Categories.Structure.Core

• Notions of Structure
• Structures
  • 9.8 The structure identity principle
    • Notion of Structure
    • Being a structure homomorphism is a preorder
    • Standard notion of structure
    • Precategory of structures

Library HoTT.Categories.Structure.IdentityPrinciple

• The Structure Identity Principle

Library HoTT.Categories.Structure.Notations

• Notations for structures

Library HoTT.Categories.Structure.Utf8

Library HoTT.Categories.UniversalProperties

• Universal morphisms
  • Initial morphisms
    • Definition
    • Introduction rule
    • Elimination rule
  • Terminal morphisms
    • Definition
    • Introduction rule
    • Elimination rule

Library HoTT.Categories.Utf8

• Unicode notations for categories

Library HoTT.Categories.Yoneda

• The Yoneda Lemma
  • Generalities
  • Formal statement
    • General version
  • The (co)yoneda functors A → (Aᵒᵖ → set)
  • The (co)yoneda lemma
  • The Yoneda embedding

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

• Homotopy coequalizers
  • Definition
  • Universal property
  • Functoriality
  • A double recursion principle
  • A double induction principle
  • Symmetry
  • Flattening

Library HoTT.Colimits.CoeqUnivProp

Library HoTT.Colimits.Colimit

• Colimits
• Existence of colimits
  • Definition of the HIT
• Functoriality of colimits
  • Colimits of equivalent diagrams
• Unicity of colimits
• Colimits are left adjoint to constant diagram

Library HoTT.Colimits.Colimit_Coequalizer

• Coequalizer as a colimit
  • Coequalizer
  • Equivalence with Coeq

Library HoTT.Colimits.Colimit_Flattening

• Flattening lemma
  • Equifibered diagrams
  • Helper lemmas
  • Main result

Library HoTT.Colimits.Colimit_Prod

• Colimit of product by a constant type

Library HoTT.Colimits.Colimit_Pushout

• Pushout as a colimit
  • PO
  • Equivalence with pushout

Library HoTT.Colimits.Colimit_Pushout_Flattening

• Pushout case

Library HoTT.Colimits.Colimit_Sigma

• Colimit of the dependent sum of a family of diagrams
  • Sigma diagrams and diagram maps / equivalences

Library HoTT.Colimits.GraphQuotient

• Quotient of a graph
  • Definition
  • The flattening lemma
  • Functoriality of graph quotients
  • Equivalence of graph quotients

Library HoTT.Colimits.MappingCylinder

• Mapping Cylinders
  • Definitions
  • Functoriality
  • Coequalizers

Library HoTT.Colimits.Pushout

• Homotopy Pushouts
  • Universal property
  • Symmetry
  • Functoriality
  • Equivalences
  • Contractibility
  • Sigmas
  • Pushouts are associative
  • Pushouts of equvialences are equivalences
  • Flattening lemma for pushouts

Library HoTT.Colimits.Quotient

• The set-quotient of a type by an hprop-valued relation
  • Quotients of kernels of maps to sets give a surjection/mono factorization.

Library HoTT.Colimits.Quotient.Choice

Library HoTT.Colimits.Sequential

Library HoTT.Colimits.SpanPushout

• Pushouts of "dependent spans".

Library HoTT.Constant

• Varieties of constant function

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

• Decidable propositions
  • Definitions
  • The type of decidable props
  • Operations
  • Computation

Library HoTT.Diagrams.Cocone

• Cocones
  • Universality of a cocone.
  • Postcomposition for cocones
  • Precomposition for cocones
  • Universality preservation

Library HoTT.Diagrams.CommutativeSquares

• Comutative squares

Library HoTT.Diagrams.Cone

• Cones
  • Precomposition for cones
  • Universality of a cone.
  • Precomposition for cones
  • Postcomposition for cones
  • Universality preservation

Library HoTT.Diagrams.ConstantDiagram

• Constant diagram

Library HoTT.Diagrams.DDiagram

Library HoTT.Diagrams.Diagram

• Diagrams
• Diagram map
  • Identity and composition for diagram maps.
• Diagram equivalences

Library HoTT.Diagrams.Graph

• Graphs

Library HoTT.Diagrams.ParallelPair

Library HoTT.Diagrams.Sequence

• Sequence

Library HoTT.Diagrams.Span

Library HoTT.Equiv.BiInv

• Bi-invertible maps

Library HoTT.Equiv.PathSplit

• n-Path-split maps.

Library HoTT.Equiv.Relational

• Relational equivalences
• Judgmental property

Library HoTT.EquivGroupoids

• The pregroupoid structure of Equiv
  • The 1-dimensional groupoid structure.
    • Theorems for moving things around in equations.

Library HoTT.ExcludedMiddle

• The law of excluded middle
  • LEM means that all propositions are decidable
  • Double-negation elimination

Library HoTT.Extensions

• Extensions and extendible maps
  • Extendability along cofibrations
  • Extendability along functor_prod
  • Extendability along functor_sigma
  • Extendability along functor_sum
  • Extendability along functor_coeq

Library HoTT.Factorization

• Factorizations and factorization systems.
  • Factorizations
  • Factorization Systems

Library HoTT.Functorish

Library HoTT.HFiber

• Basic facts about fibrations
  • The 3x3 lemma for fibrations
  • Replacing a map with a fibration
  • Exercise 4.4: The unstable octahedral axiom.
  • Fibers of constant functions
  • IsTruncMap n.+1 f ↔ IsTruncMap n (ap f)

Library HoTT.HIT.Flattening

• The flattening lemma.

Library HoTT.HIT.FreeIntQuotient

• Quotients by free actions of Int

Library HoTT.HIT.Interval

• Theorems about the homotopical interval.
  • The interval is contractible.

Library HoTT.HIT.SetCone

• Cones of HSets

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

• The set-quotient of a type by an hprop-valued relation
  • Quotients of kernels of maps to sets give a surjection/mono factorization.

Library HoTT.HIT.surjective_factor

Library HoTT.HIT.unique_choice

Library HoTT.HProp

• HPropositions
  • Alternate characterization of hprops.
  • A map is an embedding as soon as its ap's have sections.
  • Alternate characterizations of contractibility.
  • Logical equivalence of hprops
  • Inhabited and uninhabited hprops

Library HoTT.HSet

• H-Sets

Library HoTT.HoTT

Library HoTT.Homotopy.BlakersMassey

• The Generalized Blakers-Massey Theorem
  • Path algebra helper lemma
  • Setup
  • Codes
    • Right-hand codes
    • Left-hand codes
    • Codes for glue
    • Completion of codes
  • Contractibility of codes
  • The classical Blakers-Massey Theorem

Library HoTT.Homotopy.Bouquet

Library HoTT.Homotopy.CayleyDickson

Library HoTT.Homotopy.ClassifyingSpace

• We define the Classifying space of a group to be the following HIT:

Library HoTT.Homotopy.Cover

• O-connected covers
  • Functoriality of O_cover
    • Pointed functoriality
• Components

Library HoTT.Homotopy.EMSpace

Library HoTT.Homotopy.EncodeDecode

• • Encode-decode method of characterizing identity types

Library HoTT.Homotopy.EvaluationFibration

• Evaluation fibrations and self-maps

Library HoTT.Homotopy.ExactSequence

• Exact sequences
  • Very short complexes
  • Very short exact sequences and fiber sequences
  • Connecting maps
  • Long exact sequences
  • LES of loop spaces and homotopy groups
• Classifying fiber sequences

Library HoTT.Homotopy.Freudenthal

• The Freudenthal Suspension Theorem

Library HoTT.Homotopy.HSpace

Library HoTT.Homotopy.HSpace.Coherent

• • Coherent H-space structures

Library HoTT.Homotopy.HSpace.Core

• H-spaces
  • Connected H-spaces
  • Left-invertible H-spaces are homogeneous
  • Promoting unpointed homotopies to pointed homotopies

Library HoTT.Homotopy.HSpace.Moduli

• The moduli type of coherent H-space structures
  • Paths between H-space structures
  • Sections of evaluation fibrations
  • The equivalence IsCohHSpace A <~> (A ->* (A ->** A))

Library HoTT.Homotopy.HSpace.Pointwise

• Pointwise H-space structures

Library HoTT.Homotopy.HSpaceS1

Library HoTT.Homotopy.HomotopyGroup

Library HoTT.Homotopy.Hopf

• The Hopf construction
  • • Total space of the Hopf construction
  • Miscellaneous lemmas and corollaries about the Hopf construction

Library HoTT.Homotopy.Join

Library HoTT.Homotopy.Join.Core

• Joins
• Join_rec gives an equivalence of 0-groupoids
  • The graph structure on JoinRecData A B P
  • Lemmas and tactics about intervals and squares
  • Use the WildCat library to organize things
  • joinrecdata_0gpd A B is a 1-functor from Type to ZeroGpd
• Various types of equalities between paths in joins
• Functoriality of Join.
• Symmetry of Join
• Other miscellaneous results about joins

Library HoTT.Homotopy.Join.JoinAssoc

• The associativity of Join
  • The twist equivalence TriJoin A B C <~> TriJoin B A C
  • The associativity of Join
  • Naturality of trijoin_twist
  • Naturality of trijoin_id_sym
  • Naturality of join_assoc
  • The Triangle Law
  • The hexagon axiom

Library HoTT.Homotopy.Join.JoinSusp

• Join Bool A is equivalent to Susp A

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
  • Precomposition of TriJoinRecData
  • Functoriality of TriJoin via functor_trijoin
  • The relationship between functor_trijoin and functor_join.

Library HoTT.Homotopy.PinSn

• We show that the nth homotopy group of the n-sphere is the integers, for n >= 1.

Library HoTT.Homotopy.Smash

• • Miscellaneous lemmas about Smash
  • Functoriality of the smash product
  • Symmetry of the smash product

Library HoTT.Homotopy.SuccessorStructure

• Successor Structures.
  • Category of successor structures

Library HoTT.Homotopy.Suspension

• The suspension of a type
  • Eta-rule.
  • Functoriality
  • Universal property
  • Nullhomotopies of maps out of suspensions
  • Contractibility of the suspension
  • Connectedness of the suspension

Library HoTT.Homotopy.Syllepsis

Library HoTT.Homotopy.Wedge

• Wedge sums
  • • Lemmas about wedge functions
  • The pinch map on the suspension

Library HoTT.Homotopy.WhiteheadsPrinciple

Library HoTT.Idempotents

• Idempotents and their splittings
  • Basic definitions
    • Retracts
    • Splittings
    • Pre-idempotents
    • Quasi-idempotents
  • Split morphisms are quasi-idempotent
  • Quasi-idempotents split
  • Splitting already-split idempotents
  • Fully coherent idempotents
  • Quasi-idempotents need not be fully coherent
  • A pre-idempotent that is not quasi-idempotent

Library HoTT.Limits.Equalizer

Library HoTT.Limits.Limit

• Limits
• Existence of limits
• Functoriality of limits
  • Limits of equivalent diagrams
• Unicity of limits
• Limits are right adjoint to constant diagram

Library HoTT.Limits.Pullback

• Pullbacks
  • Paths in pullbacks

Library HoTT.Metatheory.Core

• Metatheory

Library HoTT.Metatheory.FunextVarieties

• Varieties of function extensionality
  • Weak funext implies Funext
  • Naive non-dependent funext implies weak funext
  • Functional extensionality is downward closed

Library HoTT.Metatheory.IntervalImpliesFunext

• Theorems about the homotopical interval.
  • From an interval type, we can prove function extensionality.

Library HoTT.Metatheory.PropTrunc

• Propositonal truncation as a colimit.

Library HoTT.Metatheory.TruncImpliesFunext

• Theorems about trunctions
  • We can construct an interval type as Trunc -1 Bool
  • From an interval type, and thus from truncations, we can prove function extensionality.

Library HoTT.Metatheory.UnivalenceImpliesFunext

• Univalence Implies Functional Extensionality

Library HoTT.Metatheory.UnivalenceVarieties

• Varieties of univalence

Library HoTT.Misc

• Miscellaneous material

Library HoTT.Modalities.Accessible

• Accessible subuniverses and modalities
  • Accessible reflective subuniverses
  • Accessible modalities

Library HoTT.Modalities.Closed

• Closed modalities

Library HoTT.Modalities.CoreflectiveSubuniverse

• Coreflective subuniverses.

Library HoTT.Modalities.Descent

• Descent between subuniverses
  • Definitions
  • Left exactness properties

Library HoTT.Modalities.Fracture

• The lex-modal fracture theorem
  • The fracture theorem
  • The fracture gluing theorem
  • The propositional fracture theorem

Library HoTT.Modalities.Identity

• The identity modality

Library HoTT.Modalities.Lex

• Lex modalities
  • Properties of lex modalities
  • Equivalent characterizations of lex-ness
  • Lex reflective subuniverses
  • Lexness via generators
  • n-fold separation

Library HoTT.Modalities.Localization

• Localization
  • Dependent extendability
  • Local types
  • Localization as a HIT
  • Localization and accessibility

Library HoTT.Modalities.Meet

Library HoTT.Modalities.Modality

• Modalities
  • Dependent eliminators
  • The strong order
  • Modalities
  • Dependent sums
  • Connectedness of the units
  • Easy modalities
  • The modal factorization system

Library HoTT.Modalities.Notnot

• The double negation modality

Library HoTT.Modalities.Nullification

• Nullification
  • Nullification and Accessibility

Library HoTT.Modalities.Open

• Open modalities
  • Definition
  • The open modality is lex
  • The open modality is accessible.

Library HoTT.Modalities.ReflectiveSubuniverse

• Reflective Subuniverses
  • References
  • Definitions
    • Subuniverses
  • Properties of Subuniverses
    • Reflections
    • Recursion principles
  • 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

• Subuniverses of separated types
  • Definition
  • Basic properties
  • Reflectiveness of Sep O
  • Left-exactness properties

Library HoTT.Modalities.Topological

• Topological localizations
  • Topological modalities are lex
  • Lex modalities generated by n-types are topological

Library HoTT.NullHomotopy

• Null homotopies of maps

Library HoTT.ObjectClassifier

• The object classifier
  • Classifying bundles with specified fiber
• The classifier for O-local types
  • Classifying O-local bundles with specified fiber
    • Classifying O-local bundles with specified pointed fiber

Library HoTT.PathAny

Library HoTT.Pointed

Library HoTT.Pointed.Core

• • Pointed Types
  • Pointed functions
  • Pointed homotopies
  • Pointed equivalences
    • Pointed products
  • 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
  • Funext for pointed types and direct consequences.
  • phomotopy_path respects 2-cells.
  • Operations on equivalences needed to make pType a wild category with equivalences
• Pointed categories give rise to pointed structures

Library HoTT.Pointed.Loops

• • Loop spaces
  • Functoriality of loop spaces
    • Properties of loops functor
    • Iterated loops functor

Library HoTT.Pointed.pEquiv

Library HoTT.Pointed.pFiber

• • Pointed fibers

Library HoTT.Pointed.pMap

• • Trivially pointed maps

Library HoTT.Pointed.pModality

• Modalities, reflective subuniverses and pointed types
  • Pointed functoriality

Library HoTT.Pointed.pSect

• Pointed sections of pointed maps

Library HoTT.Pointed.pSusp

• • Pointedness of Susp and path spaces thereof
  • Suspension Functor
  • Loop-Suspension Adjunction

Library HoTT.Pointed.pTrunc

• Truncations of pointed types
  • Functoriality of pTr
  • Truncatedness of pForall and pMap

Library HoTT.Projective

• Projective types
  • Projectivity and the axiom of choice
  • Projectivity and AC(oo,-1) (defined in HoTT book, Exercise 7.8)

Library HoTT.PropResizing.ImpredicativeTruncation

• Impredicative truncations.

Library HoTT.PropResizing.Nat

• Defining the natural numbers from univalence and propresizing.

Library HoTT.PropResizing.PropResizing

• Propositional resizing

Library HoTT.Sets.AC

• Set-theoretic formulation of the axiom of choice (AC)
• The well-ordering theorem implies AC

Library HoTT.Sets.GCH

• Formulation of GCH
• GCH is a proposition
• GCH implies LEM

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

• Hartogs number

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

• Definition of Power types
• Iterated powers

Library HoTT.Spaces.BAut

• BAut(X)
  • Basics
  • Truncation
  • Operations on BAut
  • Centers
  • Maps into BAut F classify bundles with fiber F

Library HoTT.Spaces.BAut.Bool

• BAut(Bool)
  • Nontrivial central homotopy
  • Connectedness
  • Equivalence types
  • Group structure
  • Automorphisms of BAut Bool
  • BAut (BAut Bool)

Library HoTT.Spaces.BAut.Bool.IncoherentIdempotent

• An incoherent quasi-idempotent on BAut (BAut Bool).

Library HoTT.Spaces.BAut.Cantor

• BAut(Cantor)
  • A pre-idempotent on BAut Cantor that does not split

Library HoTT.Spaces.BAut.Rigid

• Rigid types
  • HProps are rigid
  • Equivalences of BAut

Library HoTT.Spaces.Cantor

• Cantor space 2^N

Library HoTT.Spaces.Card

• • Definitions and operations
  • Properties
    • Card is a semi-ring
    • Properties of exponentiation
    • Properties of ≤
• Cardinality comparisons
• Infinity

Library HoTT.Spaces.Circle

• Theorems about the Circle.
  • The loop space of the Circle is the Integers Int
  • Connectedness and truncatedness of the Circle
  • Iteration of equivalences

Library HoTT.Spaces.Finite

Library HoTT.Spaces.Finite.Fin

• Finite sets
  • Canonical finite sets
  • Transposition equivalences
    • Swap the last two elements.
    • Swap the last element with k.
  • Equivalences between canonical finite sets
  • Initial segments of nat

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
    • Binary sums
    • Binary products
    • Function types
    • Automorphism types (i.e. symmetric groups)
  • Finite sums of natural numbers
  • Finite products of natural numbers
  • Finite subsets
  • Quotients
  • Injections
  • Surjections
  • Enumerations

Library HoTT.Spaces.Finite.Tactics

• • Tactics

Library HoTT.Spaces.Int

Library HoTT.Spaces.Int.Core

• The Integers.
  • Definition of the Integers
  • Conversion with a decimal representation for printing/parsing
  • Doubling and variants
  • Subtraction of positive into Int
  • Negation
  • Addition
  • Successor
  • Predecessor
  • Subtraction
  • Multiplication
  • Power function
  • Square
  • Sign function

Library HoTT.Spaces.Int.Equiv

• • Iteration of equivalences
    • Iteration by arbitrary integers

Library HoTT.Spaces.Int.LoopExp

• • Exponentiation of loops

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

• Lists
  • Definition
  • Length
  • Concatenation
  • Folding
  • Maps
  • Reversal
  • Getting Elements
  • Removing Elements
  • Sequences
  • Membership Predicate
  • Forall

Library HoTT.Spaces.List.Paths

• Path spaces of lists

Library HoTT.Spaces.List.Theory

• Theory of Lists and List Operations
  • Concatenation
  • Folding
  • Maps
  • Forall

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
    • Boolean equality and its properties
  • 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

• Characterization of the path types of nat

Library HoTT.Spaces.No

Library HoTT.Spaces.No.Addition

• Addition of surreal numbers

Library HoTT.Spaces.No.Core

• The surreal numbers
  • Option sorts
  • Definition
    • Games first
    • Now the surreals
    • Now the induction principle.
  • A few surreal numbers
  • More induction principles
    • The simplified induction principle for hprops
    • The non-dependent recursion principle
  • Conway's Theorem 0
  • "One-line proofs"
  • Encode-decode to characterize < and ≤ recursively (Theorem 11.6.7).
  • Changing option sorts
  • Ordinals
  • Decidable options

Library HoTT.Spaces.No.Negation

• Negation of surreal numbers

Library HoTT.Spaces.Pos

Library HoTT.Spaces.Pos.Core

• Binary Positive Integers
  • Successor
  • Properties of constructors
• 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

• • Specification of succ in term of add
  • Specification of add_carry
  • Commutativity of add
  • Permutation of add and succ
  • No neutral elements for addition
• Injectivity of pos_succ
  • Addition is associative
  • One is neutral for multiplication
  • Iteration and pos_succ
  • Right reduction properties for multiplication
  • Commutativity of multiplication
  • Distributivity of addition over multiplication
  • Associativity of multiplication
  • pos_succ and pos_mul

Library HoTT.Spaces.Spheres

• The spheres, in all dimensions.
  • Definition, by iterated suspension.
  • Pointed sphere for non-negative dimensions.
  • Explicit equivalences in low dimensions
    • Sphere 0
    • Sphere 1
    • Sphere 2
  • Truncation and connectedness of spheres.
  • Truncatedness via spheres

Library HoTT.Spaces.Torus.Torus

Library HoTT.Spaces.Torus.TorusEquivCircles

Library HoTT.Spaces.Torus.TorusHomotopy

• • Fundamental group of the torus .

Library HoTT.Spaces.TwoSphere

• Theorems about the 2-sphere S^2.

Library HoTT.Spaces.Universe

• The universe
  • Automorphisms of the universe

Library HoTT.Spectra.Spectrum

• Spectra
  • Basic Definitions of Spectra
  • Truncations of spectra

Library HoTT.Tactics

• Extra tactics for homotopy type theory.
  • Tactics for dealing with Funext
    • Tactics about transporting with path_forall
  • A more powerful variant of path_induction
• Miscellaneous tactics

Library HoTT.Tactics.BinderApply

• Apply a lemma under binders

Library HoTT.Tactics.EquivalenceInduction

• Equivalence induction

Library HoTT.Tactics.EvalIn

• Evaluating tactics on terms
  • Rewriting with reflexivity

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

• Tactics for rewriting modulo assciativity
  • Rewriting modulo associativity of composition (o)
  • Rewriting modulo associativity of concatenation (@)

Library HoTT.TruncType

• Universes of truncated types
  • Paths in TruncType
  • Some standard inhabitants
  • The canonical map from Bool to hProp
  • Facts about HProps using univalence

Library HoTT.Truncations

Library HoTT.Truncations.Connectedness

• Connectedness
  • Truncatedness of the type of extensions
  • Connectedness of path spaces
  • Connectivity of pointed types
  • Decreasing connectedness
  • 0-connectedness
  • Connectivity of the wedge into the product.

Library HoTT.Truncations.Core

• Truncations of types, in all dimensions
  • The definition
  • Trunc is a modality
  • Functoriality
  • A few special things about the (-1)-truncation
  • Tactic to remove truncations in hypotheses if possible
  • Iterated truncations

Library HoTT.Truncations.SeparatedTrunc

• • Separatedness and path-spaces of truncations

Library HoTT.Types

Library HoTT.Types.Arrow

• Theorems about Non-dependent function types
  • Paths
  • Path algebra
  • Transport
  • Dependent paths
  • Maps on paths
  • Functorial action
  • Truncatedness: functions into an n-type is an n-type
  • Functions from a contractible type
  • Equivalences
  • Decidability

Library HoTT.Types.Bool

• Theorems about the booleans
  • Decidability
  • Products as ∀ over Bool
  • The type Bool <~> Bool is equivalent to Bool.

Library HoTT.Types.Empty

• Theorems about the empty type
  • Unpacking
  • Eta conversion
  • Paths
  • Transport
  • Functorial action
  • Equivalences
  • Universal mapping properties
  • Behavior with respect to truncation
  • Paths

Library HoTT.Types.Equiv

• Equivalences

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.
  • Characterization of fiber
  • IW-types preserve truncation
  • Decidable equality for IW-types

Library HoTT.Types.Paths

• Theorems about path spaces
  • Path spaces
  • Transporting in path spaces.
  • Transporting in 2-path types
  • Functorial action
  • Equivalences between path spaces
  • Path operations are equivalences
    • Dependent paths
  • Universal mapping property
  • Truncation

Library HoTT.Types.Prod

• Theorems about cartesian products
  • Unpacking
  • Eta conversion
  • Paths
  • Transport
  • Functorial action
  • Equivalences
  • Logical equivalences
  • Symmetry
  • Associativity
  • Unit and annihilation
  • Universal mapping properties
  • Products preserve truncation
  • Decidability
  • Fibers of functor_prod

Library HoTT.Types.Sigma

• Theorems about Sigma-types (dependent sums)
  • Unpacking
  • Eta conversion
  • Paths
  • Transport
  • Functorial action
  • Equivalences
  • Associativity
  • Symmetry
  • Universal mapping properties
    • The positive universal property.
    • The negative universal property.
  • Sigmas preserve truncation
  • Subtypes (sigma types whose second components are hprops)
  • Fibers of functor_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

• Theorems about the unit type
  • Eta conversion
  • Paths
  • Transport
  • Universal mapping properties
  • Truncation
  • Equivalences

Library HoTT.Types.Universe

• Theorems about the universe, including the Univalence Axiom.
  • Paths
  • Behavior on path operations
  • Path operations vs Type operations
  • Transport
    • Transporting in particular type families
  • 2-paths
  • 3-paths
  • Equivalence induction
  • Based equivalence types
  • Truncations

Library HoTT.Types.WType

• Theorems about W-types (well-founded trees)
  • Paths
  • W-types preserve truncation

Library HoTT.Utf8

Library HoTT.Utf8Minimal

• Just enough Utf8/unicode for the Classes library to build, without depending on everything that HoTT.Utf8 depends on.

Library HoTT.WildCat

Library HoTT.WildCat.Adjoint

• • Notions of adjunctions in wild categories.
• Definition of adjunction
  • Definition of adjunction
  • Natural equivalences coming from adjunctions.
  • Building adjunctions
• Properties of adjunctions
  • Postcomposition adjunction

Library HoTT.WildCat.Bifunctor

• Bifunctors between WildCats
  • Definition
  • Bifunctor lemmas
    • 1-functorial action
    • Coherence
    • Identity preservation
    • Composition preservation
    • Equivalence preservation
    • Uncurrying
  • Flipping bifunctors
  • Composition of bifunctors
  • Natural transformations between bifunctors

Library HoTT.WildCat.Coproducts

• Categories with coproducts
  • • Codiagonal / fold map
    • Uniqueness of coproducts
    • Existence of coproducts
    • Coproduct functor
    • Categories with specific kinds of coproducts
    • Binary coproducts
    • Symmetry of coproducts
    • Associativity of coproducts
    • Binary coproduct functor
    • Coproducts in Type
  • Coproduct-product inclusions

Library HoTT.WildCat.Core

• Wild categories, functors, and transformations
  • Directed graphs
  • 0-categorical structures
  • Wild 1-categorical structures
  • Wild 1-groupoids
    • Preservation of initial and terminal objects
    • Functors preserving distinguished objects

Library HoTT.WildCat.Displayed

Library HoTT.WildCat.DisplayedEquiv

Library HoTT.WildCat.EmptyCat

Library HoTT.WildCat.Equiv

• Equivalences in wild categories
  • Movement Lemmas
  • Core of a 1-category
• 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

• Equivalences of 0-groupoids, and split essentially surjective functors

Library HoTT.WildCat.Forall

• • Indexed product of categories

Library HoTT.WildCat.FunctorCat

• Wild functor categories
  • Categories of 0-coherent 1-functors
  • Categories of 1-coherent 1-functors
• Identity functors
• Composition of functors

Library HoTT.WildCat.Induced

• Induced wild categories

Library HoTT.WildCat.Monoidal

• Monoidal Categories
  • Typeclasses for common diagrams
    • Associators
    • Unitors
    • Triangle and Pentagon identities
    • Braiding
    • Hexagon identity
  • Monoidal Categories
  • Symmetric Monoidal Categories
  • Theory about SymmetricBraid
  • Building Symmetric Monoidal Categories
    • Setup
    • Finer naturality
    • Movement lemmas
      • Moving twist
    • The associator
    • Unitors
    • Triangle
    • Pentagon
    • Hexagon
    • Conclusion

Library HoTT.WildCat.NatTrans

• • Natural transformations
    • Pointed natural transformations

Library HoTT.WildCat.Opposite

• • Opposite categories
  • Opposite functors

Library HoTT.WildCat.Paths

• Path groupoids as wild categories

Library HoTT.WildCat.PointedCat

Library HoTT.WildCat.Prod

• Product categories
  • Product functors

Library HoTT.WildCat.Products

• Categories with products
  • • Diagonal map
    • Uniqueness of products
    • Existence of products
    • Product functor
    • Categories with specific kinds of products
    • Binary products
    • Operations on indexed products
    • Binary product functor
    • Symmetry of binary products
    • Associativity of binary products
    • Products in Type

Library HoTT.WildCat.Sigma

• • Indexed sum of categories

Library HoTT.WildCat.Square

• Squares of morphisms in a Wild Category.

Library HoTT.WildCat.Sum

• • Sum categories

Library HoTT.WildCat.TwoOneCat

• Wild (2,1)-categories
  • • Whiskering functoriality
    • Exchange law

Library HoTT.WildCat.UnitCat

Library HoTT.WildCat.Universe

• • The (1-)category of types
  • The 2-category of types

Library HoTT.WildCat.Yoneda

• • Two-variable hom-functors
  • The covariant Yoneda lemma
  • The covariant Yoneda lemma using 0-groupoids
  • The contravariant Yoneda lemma
  • The contravariant Yoneda lemma using 0-groupoids

Library HoTT.WildCat.ZeroGroupoid

• The wild 1-category of 0-groupoids.
  • Tools for manipulating equivalences of 0-groupoids
  • f is an equivalence of 0-groupoids iff IsSurjInj f