Library HoTT.Contrib.HoTTBook

Library HoTT.Contrib.HoTTBookExercises

Library HoTT.Contrib.SetoidRewrite

Library HoTT.Tests.Algebra.Groups.Expressions

Library HoTT.Tests.Algebra.Groups.Group

Library HoTT.Tests.Algebra.Groups.Presentation

Library HoTT.Tests.Algebra.Rings.Expressions

Library HoTT.Tests.Algebra.Rings.Matrix

Library HoTT.Tests.Algebra.Rings.Ring

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.Spaces.List

Library HoTT.Tests.Tactics.napply

Library HoTT.Tests.Tactics.transport_paths

• • • 0 functions
    • 1 function
    • 2 functions
    • 3 functions
    • 4 functions

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.
  • Coequalizers
  • 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

• Abelianization
  • Definition of abelianization.
  • Functoriality

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

Library HoTT.Algebra.AbGroups.FiniteSum

• Finite Sums

Library HoTT.Algebra.AbGroups.FreeAbelianGroup

• Free Abelian Groups

Library HoTT.Algebra.AbGroups.TensorProduct

• The Tensor Product of Abelian Groups
  • Construction
  • Properties of tensors
  • Induction principles
  • Universal Property of the Tensor Product
  • Functoriality of the Tensor Product
  • Symmetry of the Tensor Product
  • Twisting Triple Tensors
  • Unitality of abgroup_Z
  • Symmetric Monoidal Structure of Tensor Product
  • Preservation of Coequalizers
  • Tensor Product of Free Abelian Groups
  • Tensor products distribute over direct sums

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.Categorical.MonoidObject

• Monoids and Comonoids
• Monoid objects
  • Monoid enrichment
  • Preservation of monoid objects by lax monoidal functors

Library HoTT.Algebra.Congruence

Library HoTT.Algebra.Groups

Library HoTT.Algebra.Groups.Commutator

• • Commutators of group elements
  • Easy properties of commutators
  • Hall-Witt identity
  • Precomposing normal subgroups with commutators
  • Commutator subgroups
  • Derived subgroup
    • Three subgroups lemma

Library HoTT.Algebra.Groups.Finite

• Finite Groups
  • Basic Properties
  • Lagrange's theorem

Library HoTT.Algebra.Groups.FreeGroup

• • Subgroups of free groups
  • Properties of recursor
  • Functoriality

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.
  • Cancellation lemmas
  • Group movement lemmas
    • Moving group elements
    • Moving inverses.
    • Moving elements equal to unit.
    • Cancelling elements equal to unit.
  • Commutation
  • Power operation
  • The category of Groups
  • Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms.
  • The trivial group
  • Opposite Group
  • The direct product of groups
    • Properties of maps to and from the trivial group
  • Free groups
  • Further properties of group homomorphisms.
  • Conjugation

Library HoTT.Algebra.Groups.GroupCoeq

Library HoTT.Algebra.Groups.GrpPullback

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
  • Congruence quotients
  • Sets of cosets
  • Quotient groups

Library HoTT.Algebra.Groups.ShortExactSequence

• Complexes of groups

Library HoTT.Algebra.Groups.Subgroup

• Subgroups
  • Definition of being a subgroup
  • Definition of subgroup
  • Basics properties of subgroups
  • Underlying group of a subgroup
  • Cosets of subgroups
  • Properties of left and right cosets
  • Normal subgroups
  • Trivial subgroup
  • Maximal Subgroups
  • Subgroups in opposite group
  • Preimage subgroup
  • Subgroup intersection
  • Simple groups
  • The subgroup generated by a subset
  • Product of subgroups
    • Paths between generated subgroups
  • Image of a group homomorphism
  • Image of a group embedding
  • Image of a subgroup under a group homomorphism
  • Kernels of group homomorphisms

Library HoTT.Algebra.Monoids.Monoid

• Monoids
  • Definition
  • Monoid homomorphisms
  • Basics properties of monoid homomorphisms
  • Monoid Isomorphisms
  • The category of monoids
  • Direct product of monoids

Library HoTT.Algebra.Rings

Library HoTT.Algebra.Rings.CRing

• Commutative Rings
  • Properties of commutative rings
  • Ideals in commutative rings
  • Category of commutative rings.
  • Quotient 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 generated 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
  • Preimage of ideals under ring homomorphisms
  • Extensions of ideals

Library HoTT.Algebra.Rings.Idempotent

• Idempotent elements of rings
  • Definition
    • Examples
  • Orthogonal idempotent elements
    • Properties

Library HoTT.Algebra.Rings.KroneckerDelta

• • Kronecker Delta

Library HoTT.Algebra.Rings.Localization

• Localization of commutative rings
  • Multiplicative subsets
    • Definition
    • Examples
  • Construction of localization
    • Construction of underlying Localization type
    • Addition operation
    • Multiplication operation
    • Zero element
    • One element
    • Negation operation
    • Ring laws

Library HoTT.Algebra.Rings.Matrix

• Matrices
  • Definition
  • Addition and module structure
  • Multiplication
  • Transpose
  • Diagonal matrices
  • Trace
  • Matrix minors
  • Triangular matrices
  • Symmetric Matrices
  • Skew-symmetric Matrices

Library HoTT.Algebra.Rings.Module

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

Library HoTT.Algebra.Rings.QuotientRing

• Quotient Rings
  • • Specialized induction principles
  • Quotient theory

Library HoTT.Algebra.Rings.Ring

• Rings
  • Ring laws
  • Ring movement lemmas
  • Wild category of rings
  • Subrings
  • Product ring
  • Image ring
  • Opposite Ring
  • Powers
  • Finite Sums
  • Invertible elements
    • Uniqueness of inverses
    • Closure of invertible elements under multiplication
    • Group of units
    • Multiplication by an invertible element is an equivalence
    • Invertible element movement lemmas

Library HoTT.Algebra.Rings.Vector

• Vectors
  • Definition
    • Constructors
    • Projections
    • Basic properties
  • Operations
  • Abelian group structure
  • Module structure

Library HoTT.Algebra.Rings.Z

• In this file we define the ring cring_Z of integers with underlying abelian group abgroup_Z defined in Algebra.AbGroups.Z. We also define multiplication by an integer in a general ring, and show that cring_Z is initial.

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.PropResizing

Library HoTT.Axioms.Univalence

Library HoTT.Basics

Library HoTT.Basics.Classes

• Classes
  • Injective Functions
  • Antisymmetric Relations

Library HoTT.Basics.Contractible

• Contractibility

Library HoTT.Basics.Decidable

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

Library HoTT.Basics.Equivalences

• Equivalences
  • Building equivalences between nested sigma and record types

Library HoTT.Basics.Iff

• If and only if
  • Definition
  • Basic Properties
  • Logical Laws

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.Numerals.Decimal

• Decimal numbers

Library HoTT.Basics.Numerals.Hexadecimal

• Hexadecimal numbers

Library HoTT.Basics.Overture

• Basic definitions of homotopy type theory
  • Datatypes
    • Functions
    • Option type
    • Sum type
    • Product type
  • Type classes
  • Basic definitions
    • Constant functions
  • Sigma types
  • The groupoid structure of identity types.
    • Homotopies between functions
  • Equivalences
  • Function extensionality
  • Contractibility and truncation levels
    • Truncated relations
  • Natural numbers
  • Misc
    • Pointed types
    • Homotopy fibers
  • Smallness
    • Propositional resizing

Library HoTT.Basics.PathGroupoids

• The groupoid 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.
  • Hints

Library HoTT.Basics.Settings

• General Settings
  • Warnings
  • Plugins
  • Proofs
  • Universes
  • Primitive Projections
  • Pattern Matching
  • Unification
  • Typeclasses and Hint settings
  • Reversible Coercions
  • Search Settings

Library HoTT.Basics.Tactics

• Basic tactics

Library HoTT.Basics.Trunc

• Truncatedness
  • Notation for truncation-levels
  • 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.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 precategories gives rise to an inhabitant of the path-classifying-type
  • Classify equality of precategories 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
  • Pseudofunctors from initial and terminal categories

Library HoTT.Categories.InitialTerminalCategory.Core

• Initial and terminal category definitions
  • Terminal categories
  • Initial categories
  • Default initial (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 respects 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
  • Definitions 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 equivalent to equivalences.
  • Isomorphisms in prop_cat are equivalent 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

• • • Hints for converting between types of operations

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
  • Descent
  • The flattening lemma
  • Characterization of path spaces

Library HoTT.Colimits.CoeqUnivProp

Library HoTT.Colimits.Colimit

• Colimits
  • Abstract definition
  • Existence of colimits
  • Functoriality of concrete colimits
  • Functoriality of abstract 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
  • Descent
  • The flattening lemma
  • Characterization of path spaces
  • 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 equivalences are equivalences
  • Descent
  • The flattening lemma
  • Characterization of path spaces

Library HoTT.Colimits.Quotient

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

Library HoTT.Colimits.Quotient.Choice

Library HoTT.Colimits.Sequential

• Sequential colimits

Library HoTT.Colimits.SpanPushout

• Pushouts of "dependent spans".

Library HoTT.Cubical.DPath

Library HoTT.Cubical.DPathCube

Library HoTT.Cubical.DPathSquare

Library HoTT.Cubical.PathCube

• Definition of PathCube
• PathCube reflexivity
• PathCube face rewriting
• PathCubes from paths between squares
• PathCubes from squares
• PathCube flipping
• Kan fillers
• PathCube concatenation
• natural cubes from ap

Library HoTT.Cubical.PathSquare

• Definition of PathSquare
• Degenerate PathSquares as paths between paths
• Flipping squares horizontally and vertically
• PathSquare transpose
• PathSquare inverse
• PathSquare rotations
• Edge rewriting
• Concatenation
• Kan fillers
• natural squares from ap

Library HoTT.Diagrams.Cocone

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

Library HoTT.Diagrams.CommutativeSquares

• Commutative 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 extensible 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.unique_choice

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
  • The Freudenthal Suspension Theorem

Library HoTT.Homotopy.Bouquet

Library HoTT.Homotopy.CayleyDickson

• • Cayley-Dickson spheroids
  • Negation and conjugation on suspensions
  • Cayley-Dickson imaginaroids

Library HoTT.Homotopy.ClassifyingSpace

• Classifying spaces of groups

Library HoTT.Homotopy.Cofiber

• Homotopy Cofibers
  • Definition
    • Constructors
    • Induction and recursion principles
  • Functoriality
  • Connectivity of cofibers
  • Comparison of fibers and cofibers

Library HoTT.Homotopy.Cover

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

Library HoTT.Homotopy.EMSpace

• Eilenberg-Mac Lane spaces

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.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.IdentitySystems

• Characterization of identity types by identity systems

Library HoTT.Homotopy.InjectiveTypes.InjectiveSigma

• Injectivity of Sigma types

Library HoTT.Homotopy.InjectiveTypes.InjectiveTypes

• Injective Types
  • Definitions of injectivity and first examples
  • Constructions with algebraically injective types
  • Algebraic flabbiness and resizing constructions
  • Algebraic flabbiness with resizing axioms
  • Injectivity in terms of algebraic injectivity in the absence of resizing
  • The equivalence of excluded middle with the (algebraic) injectivity of pointed types

Library HoTT.Homotopy.InjectiveTypes.TypeFamKanExt

• Kan extensions of type families

Library HoTT.Homotopy.Join

Library HoTT.Homotopy.Join.Core

• Joins
  • Zigzags in 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
  • Double recursion for Join

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.NullHomotopy

• Null homotopies of maps

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
  • Negation map

Library HoTT.Homotopy.Syllepsis

Library HoTT.Homotopy.Wedge

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

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
  • WeakFunext implies Funext
  • Naive non-dependent funext implies weak funext
  • Functional extensionality is downward closed

Library HoTT.Metatheory.ImpredicativeTruncation

• Impredicative truncations

Library HoTT.Metatheory.IntervalImpliesFunext

• An interval type implies function extensionality

Library HoTT.Metatheory.Nat

• Defining the natural numbers from univalence and propositional resizing.

Library HoTT.Metatheory.PropTrunc

• Propositional truncation as a colimit.

Library HoTT.Metatheory.TruncImpliesFunext

• Propositional truncation implies function extensionality
  • Function extensionality implies an interval type

Library HoTT.Metatheory.UnivalenceImpliesFunext

• Univalence Implies Functional Extensionality

Library HoTT.Metatheory.UnivalenceVarieties

• Varieties of univalence

Library HoTT.Misc.BarInduction

• Bar induction
  • The basic definitions
  • Relations between the three forms of bar induction
  • Examples of types that satisfy forms of bar induction
  • Implications of bar induction

Library HoTT.Misc.BoundedSearch

• Bounded Search

Library HoTT.Misc.FanTheorem

• The fan theorem

Library HoTT.Misc.UStructures

• Uniform Structures
  • nat-graded uniform structures
  • Continuity

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.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.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.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.BinInt

Library HoTT.Spaces.BinInt.Core

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

Library HoTT.Spaces.BinInt.Equiv

• • Iteration of equivalences
    • Iteration by arbitrary integers

Library HoTT.Spaces.BinInt.LoopExp

• • Exponentiation of loops

Library HoTT.Spaces.BinInt.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
  • binint_succ is a retract of binint_pred
  • binint_pred is a retract of binint_succ
  • Negation distributes over addition
  • Negation is injective
  • Subtracting 1 from a successor gives the positive integer.
  • Subtracting a successor from 1 gives minus the integer.
  • Interaction of doubling functions and subtraction
  • Subtractions cancel successors.
  • Predecessor of a subtraction is the subtraction of a successor.
  • 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.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.FreeInt

• The free group on one generator

Library HoTT.Spaces.Int

• The Integers
  • Definition
  • Number Notations
  • Successor, Predecessor and Negation
    • Successor and Predecessor
    • Negation
  • Basic Properties
    • Integer induction
    • Decidable Equality
    • Pointedness
  • Operations
    • Addition
    • Multiplication
  • Properties of Operations
    • Negation
    • Addition
    • Multiplication
  • Iteration of equivalences
    • Iteration by arbitrary integers
  • Exponentiation of loops
  • Converting between integers and naturals

Library HoTT.Spaces.List.Core

• Lists
  • Definition
  • Length
  • Concatenation
  • Folding
  • Maps - Functoriality of Lists
  • Reversal
  • Getting Elements
  • Removing Elements
  • Sequences
  • Repeat
  • Membership Predicate
  • Forall
  • Exists

Library HoTT.Spaces.List.Paths

• Path spaces of lists

Library HoTT.Spaces.List.Theory

• Theory of Lists and List Operations
  • Length
  • Concatenation
  • Folding
  • Maps
  • Reversal
  • Getting elements
  • Removing elements
    • Drop
    • Take
    • Remove
    • Filter
  • Sequences
  • Repeat
  • Forall

Library HoTT.Spaces.Nat

Library HoTT.Spaces.Nat.Arithmetic

Library HoTT.Spaces.Nat.Binomial

• Binomial coefficients
  • Definition
  • Properties

Library HoTT.Spaces.Nat.Core

• Natural numbers
  • Basic operations on naturals
    • Iteration
    • Successor and predecessor
    • Arithmetic operations
    • Maximum and minimum
    • Euclidean division
    • Greatest common divisor
  • Comparison predicates
    • Less than or equal To ≤
    • Less than <
    • Greater than or equal To ≥
    • Combined comparison predicates
  • Properties of nat_iter.
  • Properties of successors
  • Truncatedness of natural numbers
  • Properties of addition
  • Properties of multiplication
  • Basic properties of comparison predicates
    • Basic properties of ≤
    • Basic properties of <
    • Basic properties of ≥
    • Basic properties of >
  • Properties of subtraction
  • Properties of maximum and minimum
    • Properties of maximum
  • More theory of comparison predicates
    • Addition lemmas
    • Multiplication lemmas
  • Eliminating positive assumptions
    • Dichotomy of ≤
    • Trichotomy
    • Negation lemmas
    • Dichotomy of ≠
  • Arithmetic relations between trunc_index and nat.
    • Subtraction
    • Monotonicity of addition
    • Strict monotonicity of addition
    • Monotonicity of multiplication
    • Strict monotonicity of multiplication
    • Order-reflection
  • Further properties of subtraction
    • Monotonicity of subtraction
    • Order-reflection lemmas
    • Movement lemmas
  • Properties of powers
    • Monotonicity of powers
  • Strong induction
  • An induction principle for two variables with a constraint.

Library HoTT.Spaces.Nat.Division

• Division of natural numbers
  • Divisibility
  • Properties of division
  • Further Properties of division and modulo
  • Greatest Common Divisor
  • Bezout's Identity
  • Least common multiple
  • Prime Numbers
  • Composite Numbers
  • Fundamental theorem of arithmetic

Library HoTT.Spaces.Nat.Factorial

• Factorials
  • Definition
  • Properties
  • Divisibility

Library HoTT.Spaces.Nat.Paths

• Characterization of the path types of nat

Library HoTT.Spaces.NatSeq.Core

• Types of Sequences nat → X
  • Operations on sequences
  • Equivalence relations on sequences.

Library HoTT.Spaces.NatSeq.UStructure

• Uniform structure on types of sequences
  • UStructure defined by seq_agree_lt
  • Continuity

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.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 associativity
  • Rewriting modulo associativity of composition (o)
  • Rewriting modulo associativity of concatenation (@)

Library HoTT.Truncations

Library HoTT.Truncations.Connectedness

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

Library HoTT.Truncations.Constant

• Varieties of constant function

Library HoTT.Truncations.Core

• Truncations of types
  • The definition
  • Tactic to remove truncations in hypotheses if possible
  • Trunc is a modality
  • Functoriality
  • How stability and decidability interact with truncation
  • A few special things about the (-2)-truncation
  • A few special things about the (-1)-truncation
  • Surjections
  • Embeddings
  • 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
  • IsEquiv f is logically equivalent to IsTruncMap (-2) f
  • Assuming Funext, IsEquiv f is an hprop, which has further consequences
  • Other facts about 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. Well-founded 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.Option

• Option types

Library HoTT.Types.Paths

• Theorems about path spaces
  • Path spaces
  • Transporting in path spaces
    • 0 functions
    • 1 function
    • 2 functions
    • 3 functions
    • 4 functions
  • 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)
  • 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
  • Co-Unpacking
  • 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.Universes.Automorphisms

• The universe
  • Automorphisms of the universe

Library HoTT.Universes.BAut

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

Library HoTT.Universes.DProp

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

Library HoTT.Universes.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
  • Stable types and stable hprops
  • A generalization of ishprop_decpaths

Library HoTT.Universes.HSet

• H-Sets

Library HoTT.Universes.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.Universes.Rigid

• Rigid types
  • HProps are rigid
  • Equivalences of BAut

Library HoTT.Universes.Smallness

• Facts about "small" types
• Locally small types

Library HoTT.Universes.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.Universes.UniverseLevel

• Universe Levels

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
    • 1-functorial action
  • Bifunctor lemmas
    • Coherence
    • Identity preservation
    • Composition preservation
    • Equivalence preservation
  • Flipping bifunctors
  • Composition of bifunctors
  • Natural transformations between bifunctors
  • Opposite Bifunctors

Library HoTT.WildCat.Category

• Category of categories
  • Definition

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
    • Binary coproduct functor
    • Products and coproducts in the opposite category
    • Symmetry of coproducts
    • Associativity of coproducts
    • Codiagonal
    • Lemmas about cat_bincoprod_rec
    • Cocartesian Monoidal Structure
    • Coproducts in Type
  • Canonical coproduct-product map
    • Coproducts in the opposite category

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
• Opposite categories preserve having equivalences.
  • 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.Graph

• Category of graphs
  • Definition
  • Category of graphs

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 Associator
  • Theory about LeftUnitor and RightUnitor
  • Theory about Braiding
  • Theory about SymmetricBraid
  • Opposite Monoidal Categories
  • Further Coherence Conditions
  • Monoidal functors

Library HoTT.WildCat.MonoidalTwistConstruction

• Building Symmetric Monoidal Categories
  • • Setup
    • Finer naturality
    • Movement lemmas
      • Moving twist
    • The associator
    • Unitors
    • Triangle
    • Pentagon
    • Hexagon
    • Conclusion

Library HoTT.WildCat.NatTrans

• Wild Natural Transformations
  • Transformations
    • Definition
  • Naturality
  • Natural transformations
  • Natural equivalences
  • 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
    • Diagonal
    • Lemmas about cat_binprod_corec
    • 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