Development of homotopy type theory in Agda
This repository contains a development of homotopy type theory and univalent foundations in Agda. The structure of the source code is described below.
The code is loosely broken into hott-core
and hott-theorems
Agda libraries.
You need Agda 2.5.3
and include at least the path to hott-core.agda-lib
in your Agda library list.
See CHANGELOG
of Agda 2.5 for more information.
Support for Agda 2.5.4 or newer is currently lacking.
Each Agda file should have --without-K --rewriting
in its header.
--without-K
is to restrict pattern matching so that the uniqueness of identity proofs is not admissible,
and --rewriting
is for the computational rules of the higher inductive types.
is-prop
)TODO: principles of variable names
The identity type is _==_
, because _=_
is not allowed in Agda. For every
identifier talking about the identity type, the single symbol =
is used
instead, because this is allowed by Agda. For instance the introduction rule for
the identity type of Σ-types is pair=
and not pair==
.
The numbering is the homotopy-theoretic numbering, parametrized by the type
TLevel
or ℕ₋₂
where
data TLevel : Type₀ where
⟨-2⟩ : TLevel
S : TLevel → TLevel
ℕ₋₂ = TLevel
Numeric literals (including negative ones) are overloaded.
There is also explicit conversion ⟨_⟩ : ℕ → ℕ₋₂
with the obvious definition.
Names of the form is-X
or has-X
, represent properties that can hold (or not)
for some type A
. Such a property can be parametrized by some arguments. The
property is said to hold for a type A
iff is-X args A
is inhabited. The
types is-X args A
should be (h-)propositions.
Examples:
is-contr
is-prop
is-set
has-level -- This one has one argument of type [ℕ₋₂]
has-all-paths -- Every two points are equal
has-dec-eq -- Decidable equality
A
(perhaps with arguments) has some
property is-X
is named A-is-X
. The arguments of A-is-X
are the arguments
of is-X
followed by the arguments of A
.is-X
also satisfies is-Y
are
named X-is-Y
(and not is-X-is-Y
which would mean is-Y (is-X A)
).Examples (only the nonimplicit arguments are given)
Unit-is-contr : is-contr Unit
Bool-is-set : is-set Bool
is-contr-is-prop : is-contr (is-prop A)
contr-is-prop : is-contr A → is-prop A
dec-eq-is-set : has-dec-eq A → is-set A
contr-has-all-paths : is-contr A → has-all-paths A
The term giving the most natural truncation level to some type constructor T is
called T-level
:
Σ-level : (n : ℕ₋₂) → (has-level n A) → ((x : A) → has-level n (P x))
→ has-level n (Σ A P)
×-level : (n : ℕ₋₂) → (has-level n A) → (has-level n B)
→ has-level n (A × B))
Π-level : (n : ℕ₋₂) → ((x : A) → has-level n (P x))
→ has-level n (Π A P)
→-level : (n : ℕ₋₂) → (has-level n B)
→ has-level n (A → B))
Similar suffices include conn
for connectivity.
Modules of the same name as a type collects useful properties given an element of that type. Records have this functionality built-in.
A
and B
is often called A-to-B
f : A → B
, the lemma asserting that f
is an equivalence is called
f-is-equiv
.f : A → B
, the equivalence (f , f-is-equiv)
is called f-equiv
.A-to-B-equiv
is usually called
A-equiv-B
instead.We have
A-to-B : A → B
A-to-B-is-equiv : is-equiv (A-to-B)
A-to-B-equiv : A ≃ B
A-equiv-B : A ≃ B
A-to-B-path : A == B
A-is-B : A == B
Also for group morphisms, we have
G-to-H : G →ᴳ H
G-to-H-is-iso : is-equiv (fst G-to-H)
G-to-H-iso : G ≃ᴳ H
G-iso-H : G ≃ᴳ H
However, A-is-B
can be easily confused with is-X
above,
so it should be used with great caution.
Another way of naming of equivalences only specifies one side.
Suffixes -econv
may be added for clarity.
The suffix -conv
refers to the derived path.
A : A == B
A-econv : A ≃ B
A-conv : A == B
TODO: pres
and preserves
.
TODO: -inj
and -surj
for injectivity and surjectivity.
TODO: -nat
for naturality.
The constructor of a record should usually be the uncapitalized name of the
record. If N
is a negative type (for instance a record) with introduction
rule n
and elimination rules e1
, …, en
, then
N
is called N=
N
are called n=
and
e1=
, …, en=
N==
and similarly for the
intros and elim.N
are called e1=-β
, …,
en=-β
.n=-η
(TODO: maybe N=-η
instead, or
additionally?)N=
and _==_ {N}
is calledN=-equiv
/N=-path
(TODO: n=-equiv
/n=-path
would maybe be more natural).
Note that this equivalence is usually needed in the direction N= ≃ _==_ {N}
If a positive type N
behaves like a negative one through
some access function f : N → M
,
the property is called f-ext : (n₁ n₂ : N) → f n₁ = f n₂ → n₁ = n₂
A family of some structures indexed by another structures often behaves like a functor which maps functions between structures to functions between corresponding structures. Here is a list of standardized suffices that denote different kind of functoriality:
X-fmap
: X
maps morphisms to morphisms (covariantly or contravariantly).X-csmap
: X
maps commuting squares to commuting squares (covariantly or contravariantly).X-emap
: X
maps isomorphisms to isomorphisms.X-isemap
: Usually a part of X-emap
which lifts the proof of being an isomorphism.For types, morphisms are functions and isomorphisms are equivalences. Bi-functors are not standardized (yet).
TODO: X-fmap-id
, X-fmap-∘
Precedence convention
_$_
and arrows: 0_,_
): 60_×_
): 80See core/lib/types/Pushout.agda
for an example of higher inductive types.
Constructors should make all the parameters implicit, and varients which make
commonly specified parameters explicit should have the suffix '
.
S0
is defined as Bool
, and the circle is the suspension of Bool
.
The structure of the source is roughly the following:
old/
)The old library is still present, mainly to facilitate code transfer to the new library. Once everything has been ported to the new library, this directory will be removed.
core/
)The main library is more or less divided in three parts.
lib.Basics
and contains everything
needed to make the second part compilelib.types.Types
and contains
everything you ever wanted to know about all type formersThe whole library is exported in the file HoTT
, so every file using the
library should contain open import HoTT
.
TODO: describe more precisely each file
theorems/homotopy/
)This directory contains proofs of interesting homotopy-theoretic theorems.
3x3/
: Contains definitions and lemmas for the 3x3-lemma stating that pushouts commute with pushouts.
Commutes
: Proves the main result of the 3x3-lemma, see Guillaume Brunerie's thesis.AnyUniversalCoverIsPathSet
: Proves that for any universal covering F
over some type A
with base point a₁ : A
, the fiber F.Fiber a₂
over some point a₂ : A
is equivalent to a₁ =₀ a₂
, the 0-truncation of the space of paths between a₁
and a₂
.BlakersMassey
: Contains a proof of the Blakers–Massey theorem. See the paper A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory and Favonia's thesis.blakersmassey/
: Contains definitions and lemmas for BlakersMassey.agda
.Bouquet
: Defines the bouquet of a family of circles and other families of pointed types.CircleCover
: Defines a type S¹Cover
and proves that it is equivalent to the type Cover S¹ j
of coverings of S¹
.CircleHSpace
: Defines ⊙S¹-hSpace : HSpaceStructure ⊙S¹
.CoHSpace
: Defines what a CoHSpaceStructure
is.CofiberComp
: Let f : X ⊙→ Z
and g : Y ⊙→ Z
be two pointed maps. This file proves that the cofiber of the composition of g
and ⊙cfcod` f : Z ⊙→ ⊙Cofiber f
is equivalent to the cofiber of the induced map h : X ⊙∨ Y ⊙→ Z
.CofiberSequence
: Proves that the 5-term sequence obtained from a map f : X ⊙→ Y
by repeatedly taking the map into the cofiber of the previous map is equivalent to the sequence X ⊙→⟨ f ⟩ Y ⊙→⟨ ⊙cfcod` f ⟩ ⊙Cofiber f ⊙→⟨ ⊙extract-glue ⟩ ⊙Susp X ⊙→⟨ ⊙Susp-fmap f ⟩ ⊙Susp Y ⊙⊣|
.Cogroup
: Defines CogroupStructure
, proves that such a structure on X
induces a GroupStructure
on X ⊙→ Y
for any pointed type Y
.ConstantToSetExtendsToProp
: Proves that any constant function f : A → B
factors through a function Trunc -1 A → B
.DisjointlyPointedSet
: Defines properties is-separable X
(equality to the base point is decidable) and has-disjoint-pt
(being pointedly equivalent to the coproduct of the singleton and MinusPoint X
, that is X
without the base point) of pointed types X
and proves that they are equivalent. Also gives a pointed equivalence between ⊙Bouquet (MinusPoint X) 0
, a bouquet of 0-spheres indexed by MinusPoint X
and X
for each pointed type X
that is separable.elims/
: Contains proofs of elimination principles.
CofPushoutSection
: Given a span s
, in which one of the maps has a left-inverse, and a map h : Pushout s → D
, proves an elimination principle for Cofiber h
.Lemmas
: Contains technical lemmas about commutative squares over commutative squares.SuspSmash
: Gives an elimination principle for Susp (X ∧ Y)
, the suspension of the smash product.EM1HSpace
: Defines the HSpaceStructure
on the Eilenberg–MacLane space ⊙EM₁ G
for an abelian group G
.EilenbergMacLane
: Defines the Eilenberg–MacLane spaces ⊙EM G n
, proves that ⊙Ω (⊙EM G (S n))
is pointedly equivalent to ⊙EM G n
for each n
and that their homotopy groups are as required. See Eilenberg-MacLane Spaces in Homotopy Type Theory by Dan Licata and Eric Finster.EilenbergMacLane1
: Proves that the fundamental group of the Eilenberg–MacLane space ⊙EM₁ G
(which is defined as a HIT) is in fact G
.FiberOfWedgeToProduct
: Let X
of Y
be two types with basepoints x₀
and y₀
. This contains a proof that the fiber of the induced map X ∨ Y → X × Y
over a point (x , y)
is equivalent to the join (x₀ == x) * (y₀ == y)
.FinSet
: Equivalence between two different definitions of finite sets.FinWedge
: Contains helper functions and lemmas for dealing with wedges indexed over Fin I
for some I : ℕ
.Freudenthal
: Proves the Freudenthal suspension theorem.GroupSetsRepresentCovers
: Let X
be a 0-connected type. This file gives an equivalence between coverings of X
and πS 0 X
-sets (where πS 0 X
is the fundamental group of X
).HSpace
: Contains definition(s) of H-spaces and some basic lemmas.Hopf
: Proves that the total space of the Hopf fibration is S³
.HopfConstruction
: Given a 0-connected H-space X
, constructs a fibration H
on Susp A
with total space equivalent to the join X * X
.HopfJunior
: Contains HopfJunior : S¹ → Type₀
, a fibration with fibers equivalent to Bool
(a.k.a. the 0-sphere) and a proof that its total space is (equivalent to) S¹
.IterSuspensionStable
: Contains a reformulation of the Freudenthal suspension theorem.JoinAssoc3x3
: Gives an equivalence between the joins (A * B) * C
and A * (B * C)
. The proof uses the 3x3-lemma.JoinAssocCubical
: Gives an equivalence between the joins (A * B) * C
and A * (B * C)
. The proof involves squares and cubes.JoinComm
: Gives an equivalence between the joins A * B
and B * A
.JoinSusp
: Contains equivalences Bool * A ≃ Susp A
, Susp A * B ≃ Susp (A * B)
and ⊙Sphere m ⊙* X ⊙≃ ⊙Susp^ (S m) X
((m+1)-fold suspension is equivalent to joining with an m-sphere).LoopSpaceCircle
: Proves that the fundamental group of the circle is equivalent to the integers.ModalWedgeExtension
: Lemmas about modalities and the function X ∨ Y → X × Y
for pointed types X
and Y
.Pigeonhole
: The finite pigeonhole principle.PathSetIsInitalCover
: Proves that the covering constructed from the path set of a type X
is initial in the category of coverings of X
.Pi2HSusp
: Given an H-space X
, constructs an isomorphism π₂-Susp : πS 1 (⊙Susp X) ≃ᴳ πS 0 X
between the fundamental group of X
and the second homotopy group of its suspension.PinSn
: Proves that the n-th homotopy group of the n-sphere is isomorphic to the integers.PropJoinProp
: Proves that if A
and B
are propositions, then so is A * B
.PtdAdjoint
: Defines what a endofunctor of the category of pointed spaces is, gives two definitions of adjointness of such functors via unit and counit morphisms and via equivalence of Hom-types and constructs equivalence between the definitions. Also proves that right adjoints preserve products and left adjoints preserve wedges.PtdMapSequence
: Defines data types representing sequences of pointed maps and maps between them.PushoutSplit
: Shows one direction of the pasting law for pushouts, namely the fact that if you compose pushout squares you get another pushout square.RelativelyConstantToSetExtendsViaSurjection
: Given a surjective function f : A → B
, a type family C : B → Type k
of sets and a dependent function g : (a : A) → C (f a)
such that g
agree g-is-const : ∀ a₁ a₂ → (p : f a₁ == f a₂) → g a₁ == g a₂ [ C ↓ p ]
, shows that there is a function ext : (b : B) → C (f a)
such that g
is equal to ext ∘ f
.RibbonCover
: Constructs a covering of a type X
given a set with an action of the fundamental group of X
on it. Used to prove an equivalence between such sets and coverings if X
is connected in GroupSetsRepresentCovers
.SmashIsCofiber
: Proves that the smash product Smash X Y
of two pointed types X
and Y
is equivalent to the cofiber of the induced map A ∨ B → A × B
.SpaceFromGroups
: Given an infinite sequence of groups, all abelian except maybe the first, constructs a type with these groups as its homotopy groups.SphereEndomorphism
: Proves that the types of endomaps of a sphere and the type of basepoint-preserving such endomaps become equivalent when 0-truncated. Also proves that suspension induces an equivalence between the set of endomaps of the n
-sphere and the set of endomaps of the S n
-sphere for positive n
.SuspAdjointLoop
: Defines the suspension and the loop functor and proves that they are adjoint.SuspAdjointLoopLadder
: Proves naturality in the covariant argument of the adjunction between the iterated suspension and the iterated loop space when phrased in terms of Hom-types.SuspProduct
: Proves that ⊙Susp (X ⊙× Y) ⊙≃ ⊙Susp X ⊙∨ (⊙Susp Y ⊙∨ ⊙Susp (X ⊙∧ Y))
.SuspSectionDecomp
: Let f : X → Y
be a pointed section of g : Y → X
. Then there is an equivalence Susp (de⊙ Y) ≃ ⊙Susp X ∨ ⊙Susp (⊙Cofiber ⊙f)
between the suspension of Y
and the wedge sum of the suspensions of X
and the cofiber of f
. This can be interpreted as a splitting in the part ΣX → ΣY → Σcofib(f) of the cofiber sequence of f
.SuspSmashJoin
: Gives an equivalence ⊙Susp (⊙Smash X Y) ⊙≃ (X ⊙* Y)
between the suspension of the smash product and the join of two pointed types.TruncationLoopLadder
: Proves the naturality of the equivalence of the 0-truncation of the m-fold loop space and the m-fold loop space of the m-truncation.VanKampen
: Proves the improved version of the Seifert–van Kampen theorem for calculating the fundamental groupoid of a pushout from Favonia's thesis.vankampen/
: Contains definitions and lemmas for VanKampen.agda
.WedgeCofiber
: Shows that the cofiber space of winl : X → X ∨ Y
is equivalent to Y
and the cofiber space of winr : Y → X ∨ Y
is equivalent to X
.WedgeExtension
: Proves the wedge connectivity lemma from the HoTT book (lemma 8.6.2), which basically says that given an n-connected pointed type A
and an m-connected pointed type B
a function h : (w : A ∨ B) → P (∨-to-× w)
, where P : A × B → Type
is a family of (n+m)-types, extends along ∨-to-× : A ∨ B → A × B
.theorems/cohomology/
)This directory contains proofs of interesting cohomology-theoretic theorems. Many results in this directory are described in Evan Cavallo's thesis.
Bouquet
: Shows that the cohomology in degree n of a bouquet of n-spheres indexed by a type I
, which has choice, is isomorphic to the product of I
copies of C2 0
(the 0-th cohomology of the 0-sphere) for an ordinary cohomology theory.ChainComplex
: Defines the data types of (co)chain complexes and equivalences between them, defines their (co)homology groups and proves that equivalences between complex induce equivalences between their cohomology groups.CoHSpace
: Contains simple lemmas about the cohomology of co-H-spaces.Cogroup
: Given a type X
with a cogroup structure and a type Y
, proves that the map (X ⊙→ Y) → (C n Y →ᴳ C n X)
is a group homomorphism for any cohomology theory C
.Coproduct
: Proves that C n (X ⊙⊔ Y) ≃ᴳ C n (X ⊙∨ Y) ×ᴳ C2 n
(where C2 n
is the n
-th cohomology of the 0-sphere) for any cohomology theory C
.DisjointlyPointedSet
: Shows that the cohomology of a separable pointed set X
, which has choice, is the MinusPoint X
-fold product of C2 0
(the 0-th cohomology of the 0-sphere) in degree 0 and trivial in higher degrees for any ordinary cohomology theory C
.EMModel
: Constructs the Eilenberg–MacLane spectrum given an abelian group and shows that its induced cohomology theory is ordinary.InverseInSusp
: Shows that the homomorphism Cⁿ(ΣX) → Cⁿ(ΣX) mapping an element to its inverse is induced by a map ΣX → ΣX.LongExactSequence
: Given a map f : X → Y
, constructs the sequence Cⁿ(Y) → Cⁿ(X) → Cⁿ⁺¹(cofib(f)) → Cⁿ⁺¹(Y) → ⋯ and shows that it is exact.MayerVietoris
: Given a pointed span X ←f– Z –g→ Y, shows the cofiber space of the natural map reglue
: X ∨ Y → X ⊔_Z Y is equivalent to the suspension of Z. Using this equivalence one can derive the Mayer–Vietoris sequence from the long exact sequence associated with reglue
.PtdMapSequence
: Functions for applying a cohomology theory to a sequence of pointed maps, producing a sequence of group homomorphisms.RephraseSubFinCoboundary
: Gives a description the homomorphism induced in cohomology by a map from a bouquet of (n+1)-spheres to the suspension of a bouquet of n-spheres in terms of mapping degrees. This is used for defining cellular cohomology.Sigma
: Constructs an isomorphism C n (⊙Σ X Y) ≃ᴳ C n (⊙BigWedge Y) ×ᴳ C n X
for a type X
, a family Y : X → Ptd i
and any cohomology theory C
.SpectrumModel
: Shows that a spectrum induces a cohomology theory.Sphere
: Shows that the cohomology of the m-sphere is C2 0
(the 0-cohomology of the 0-sphere) in degree m and trivial in other degrees for any ordinary cohomology theory.SphereEndomorphism
: Proves that the map C n (⊙Sphere (S m)) C → n (⊙Sphere (S m))
induced by a map f : ⊙Sphere (S m) ⊙→ ⊙Sphere (S m)
is given by multiplication with the degree of f
.SphereProduct
: Gives an isomorphism C n (⊙Sphere m ⊙× X) ≃ᴳ C n (⊙Lift (⊙Sphere m)) ×ᴳ (C n X ×ᴳ C n (⊙Susp^ m X))
for calculating the cohomology of the product of the m-sphere and X
for any pointed type X
and any cohomology theory.SubFinBouquet
: Constructs an explicit inverse to the function from the cohomology of the wedge of m-spheres indexed over a subfinite type B
to the product (indexed over B
) of the 0-th cohomology groups of the 0-sphere.SubFinWedge
: Constructs an explicit inverse to the function from the cohomology of the wedge of a (sub)finite family of pointed types to the product of the cohomologies of the pointed types.Theory
: Defines a data type CohomologyTheory
of cohomology theories fulfilling some axioms similar to the Eilenberg–Steenrod axioms and proves some basic consequences of these axioms.Torus
: Contains a computation of the cohomology of the n-torus.Wedge
: Gives an isomorphism between Cⁿ(X ∨ Y) and Cⁿ(X) × Cⁿ(Y) (“finite additivity”) without using the additivity axiom and shows that e.g. the projection map to Cⁿ(X) is induced by the inclusion of X in X ∨ Y and similarly for other maps.theorems/cw/
)This directory contains proofs of interesting theorems about CW complexes.
TODO: describe more precisely each file
stash/
)This directory contains experimental or unfinished work.
@online{hott-in:agda,
author={Guillaume Brunerie
and Kuen-Bang {Hou (Favonia)}
and Evan Cavallo
and Tim Baumann
and Eric Finster
and Jesper Cockx
and Christian Sattler
and Chris Jeris
and Michael Shulman
and others},
title={Homotopy Type Theory in {A}gda},
url={https://github.com/HoTT/HoTT-Agda}
}
Names are roughly sorted by the amount of contributed code, with the founder Guillaume always staying on the top. List of contribution (possibly outdated or incorrect):
This work is released under MIT license. See LICENSE.md.
This material was sponsored by the National Science Foundation under grant numbers CCF-1116703 and DMS-1638352; Air Force Office of Scientific Research under grant numbers FA-95501210370 and FA-95501510053. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government or any other entity.