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.
- Line length should be reasonably short, not much more than 80 characters (TODO: except maybe sometimes for equational reasoning?)
- Directories are in lowercase and modules are in CamelCase
- Types are Capitalized unless they represent properties (like
is-prop
) - Terms are in lowercase-with-hyphens-between-words unless the words refer to types.
- Try to avoid names of free variables in identifiers
- Pointedness and other disambiguating labels may be omitted if inferable from prefixes.
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
- The theorem stating that some type
A
(perhaps with arguments) has some propertyis-X
is namedA-is-X
. The arguments ofA-is-X
are the arguments ofis-X
followed by the arguments ofA
. - Theorems stating that any type satisfying
is-X
also satisfiesis-Y
are namedX-is-Y
(and notis-X-is-Y
which would meanis-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 natural function between two types
A
andB
is often calledA-to-B
- If
f : A → B
, the lemma asserting thatf
is an equivalence is calledf-is-equiv
. - If
f : A → B
, the equivalence(f , f-is-equiv)
is calledf-equiv
. - As a special case of the previous point,
A-to-B-equiv
is usually calledA-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
- The identity type on
N
is calledN=
- The intros and elim rules for the identity type on
N
are calledn=
ande1=
, …,en=
- If necessary, the double identity type is called
N==
and similarly for the intros and elim. - The β-elimination rules for the identity type on
N
are callede1=-β
, …,en=-β
. - The η-expansion rule is called
n=-η
(TODO: maybeN=-η
instead, or additionally?) - The equivalence/path between
N=
and_==_ {N}
is called N=-equiv
/N=-path
(TODO:n=-equiv
/n=-path
would maybe be more natural). Note that this equivalence is usually needed in the directionN= ≃ _==_ {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 ofX-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
- Separators
_$_
and arrows: 0 - Layout combinators (equational reasoning): 10-15
- Equalities, equivalences: 30
- Other relations, operators with line-level separators: 40
- Constructors (for example
_,_
): 60 - Binary operators (including type formers like
_×_
): 80 - Prefix operators: 100
- Postfix operators: 120
-
See
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 asBool
, and the circle is the suspension ofBool
.
The structure of the source is roughly the following:
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.
The main library is more or less divided in three parts.
- The first part is exported in the module
lib.Basics
and contains everything needed to make the second part compile - The second part is exported in the module
lib.types.Types
and contains everything you ever wanted to know about all type formers - The third part contains more advanced stuff.
The 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
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 coveringF
over some typeA
with base pointa₁ : A
, the fiberF.Fiber a₂
over some pointa₂ : A
is equivalent toa₁ =₀ a₂
, the 0-truncation of the space of paths betweena₁
anda₂
.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 forBlakersMassey.agda
.Bouquet
: Defines the bouquet of a family of circles and other families of pointed types.CircleCover
: Defines a typeS¹Cover
and proves that it is equivalent to the typeCover S¹ j
of coverings ofS¹
.CircleHSpace
: Defines⊙S¹-hSpace : HSpaceStructure ⊙S¹
.CoHSpace
: Defines what aCoHSpaceStructure
is.CofiberComp
: Letf : X ⊙→ Z
andg : Y ⊙→ Z
be two pointed maps. This file proves that the cofiber of the composition ofg
and⊙cfcod` f : Z ⊙→ ⊙Cofiber f
is equivalent to the cofiber of the induced maph : X ⊙∨ Y ⊙→ Z
.CofiberSequence
: Proves that the 5-term sequence obtained from a mapf : X ⊙→ Y
by repeatedly taking the map into the cofiber of the previous map is equivalent to the sequenceX ⊙→⟨ f ⟩ Y ⊙→⟨ ⊙cfcod` f ⟩ ⊙Cofiber f ⊙→⟨ ⊙extract-glue ⟩ ⊙Susp X ⊙→⟨ ⊙Susp-fmap f ⟩ ⊙Susp Y ⊙⊣|
.Cogroup
: DefinesCogroupStructure
, proves that such a structure onX
induces aGroupStructure
onX ⊙→ Y
for any pointed typeY
.ConstantToSetExtendsToProp
: Proves that any constant functionf : A → B
factors through a functionTrunc -1 A → B
.DisjointlyPointedSet
: Defines propertiesis-separable X
(equality to the base point is decidable) andhas-disjoint-pt
(being pointedly equivalent to the coproduct of the singleton andMinusPoint X
, that isX
without the base point) of pointed typesX
and proves that they are equivalent. Also gives a pointed equivalence between⊙Bouquet (MinusPoint X) 0
, a bouquet of 0-spheres indexed byMinusPoint X
andX
for each pointed typeX
that is separable.elims/
: Contains proofs of elimination principles.CofPushoutSection
: Given a spans
, in which one of the maps has a left-inverse, and a maph : Pushout s → D
, proves an elimination principle forCofiber h
.Lemmas
: Contains technical lemmas about commutative squares over commutative squares.SuspSmash
: Gives an elimination principle forSusp (X ∧ Y)
, the suspension of the smash product.
EM1HSpace
: Defines theHSpaceStructure
on the Eilenberg–MacLane space⊙EM₁ G
for an abelian groupG
.EilenbergMacLane
: Defines the Eilenberg–MacLane spaces⊙EM G n
, proves that⊙Ω (⊙EM G (S n))
is pointedly equivalent to⊙EM G n
for eachn
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 factG
.FiberOfWedgeToProduct
: LetX
ofY
be two types with basepointsx₀
andy₀
. This contains a proof that the fiber of the induced mapX ∨ 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 overFin I
for someI : ℕ
.Freudenthal
: Proves the Freudenthal suspension theorem.GroupSetsRepresentCovers
: LetX
be a 0-connected type. This file gives an equivalence between coverings ofX
andπS 0 X
-sets (whereπS 0 X
is the fundamental group ofX
).HSpace
: Contains definition(s) of H-spaces and some basic lemmas.Hopf
: Proves that the total space of the Hopf fibration isS³
.HopfConstruction
: Given a 0-connected H-spaceX
, constructs a fibrationH
onSusp A
with total space equivalent to the joinX * X
.HopfJunior
: ContainsHopfJunior : S¹ → Type₀
, a fibration with fibers equivalent toBool
(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
andA * (B * C)
. The proof uses the 3x3-lemma.JoinAssocCubical
: Gives an equivalence between the joins(A * B) * C
andA * (B * C)
. The proof involves squares and cubes.JoinComm
: Gives an equivalence between the joinsA * B
andB * A
.JoinSusp
: Contains equivalencesBool * 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 functionX ∨ Y → X × Y
for pointed typesX
andY
.Pigeonhole
: The finite pigeonhole principle.PathSetIsInitalCover
: Proves that the covering constructed from the path set of a typeX
is initial in the category of coverings ofX
.Pi2HSusp
: Given an H-spaceX
, constructs an isomorphismπ₂-Susp : πS 1 (⊙Susp X) ≃ᴳ πS 0 X
between the fundamental group ofX
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 ifA
andB
are propositions, then so isA * 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 functionf : A → B
, a type familyC : B → Type k
of sets and a dependent functiong : (a : A) → C (f a)
such thatg
agreeg-is-const : ∀ a₁ a₂ → (p : f a₁ == f a₂) → g a₁ == g a₂ [ C ↓ p ]
, shows that there is a functionext : (b : B) → C (f a)
such thatg
is equal toext ∘ f
.RibbonCover
: Constructs a covering of a typeX
given a set with an action of the fundamental group ofX
on it. Used to prove an equivalence between such sets and coverings ifX
is connected inGroupSetsRepresentCovers
.SmashIsCofiber
: Proves that the smash productSmash X Y
of two pointed typesX
andY
is equivalent to the cofiber of the induced mapA ∨ 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 then
-sphere and the set of endomaps of theS n
-sphere for positiven
.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
: Letf : X → Y
be a pointed section ofg : Y → X
. Then there is an equivalenceSusp (de⊙ Y) ≃ ⊙Susp X ∨ ⊙Susp (⊙Cofiber ⊙f)
between the suspension ofY
and the wedge sum of the suspensions ofX
and the cofiber off
. This can be interpreted as a splitting in the part ΣX → ΣY → Σcofib(f) of the cofiber sequence off
.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 forVanKampen.agda
.WedgeCofiber
: Shows that the cofiber space ofwinl : X → X ∨ Y
is equivalent toY
and the cofiber space ofwinr : Y → X ∨ Y
is equivalent toX
.WedgeExtension
: Proves the wedge connectivity lemma from the HoTT book (lemma 8.6.2), which basically says that given an n-connected pointed typeA
and an m-connected pointed typeB
a functionh : (w : A ∨ B) → P (∨-to-× w)
, whereP : A × B → Type
is a family of (n+m)-types, extends along∨-to-× : A ∨ B → A × B
.
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 typeI
, which has choice, is isomorphic to the product ofI
copies ofC2 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 typeX
with a cogroup structure and a typeY
, proves that the map(X ⊙→ Y) → (C n Y →ᴳ C n X)
is a group homomorphism for any cohomology theoryC
.Coproduct
: Proves thatC n (X ⊙⊔ Y) ≃ᴳ C n (X ⊙∨ Y) ×ᴳ C2 n
(whereC2 n
is then
-th cohomology of the 0-sphere) for any cohomology theoryC
.DisjointlyPointedSet
: Shows that the cohomology of a separable pointed setX
, which has choice, is theMinusPoint X
-fold product ofC2 0
(the 0-th cohomology of the 0-sphere) in degree 0 and trivial in higher degrees for any ordinary cohomology theoryC
.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 mapf : 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 mapreglue
: 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 withreglue
.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 isomorphismC n (⊙Σ X Y) ≃ᴳ C n (⊙BigWedge Y) ×ᴳ C n X
for a typeX
, a familyY : X → Ptd i
and any cohomology theoryC
.SpectrumModel
: Shows that a spectrum induces a cohomology theory.Sphere
: Shows that the cohomology of the m-sphere isC2 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 mapC n (⊙Sphere (S m)) C → n (⊙Sphere (S m))
induced by a mapf : ⊙Sphere (S m) ⊙→ ⊙Sphere (S m)
is given by multiplication with the degree off
.SphereProduct
: Gives an isomorphismC 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 andX
for any pointed typeX
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 typeB
to the product (indexed overB
) 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 typeCohomologyTheory
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.
This directory contains proofs of interesting theorems about CW complexes.
TODO: describe more precisely each file
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):
- Guillaume Brunerie: the foundation, pi1s1, 3x3 lemma, many more
- Favonia: covering space, Blakers-Massey, van Kampen, cohomology
- Evan Cavallo: cubical reasoning, cohomology, Mayer-Vietoris
- Tim Baumann: cup product
- Eric Finster: modalities
- Jesper Cockx: rewrite rules
- Christian Sattler: updates to equivalence and univalence
- Chris Jeris: Eckmann-Hilton argument
- Michael Shulman: updates to equivalence and univalence
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.