This is an attempt to develop Homotopy Type Theory in Lean 4.
As in gebner/hott3, no modifications to the Lean kernel are made, because library uses large eliminator checker ported from Lean 3. So stuff like this will print an error:
hott theorem Id.UIP {α : Type u} {a b : α} (p q : a = b) : p = q :=
begin cases p; cases q; apply Id.refl end
Most HITs in the library constructed using quotients. Quotients in Lean have good computational properties (Quot.ind
computes), so we can define HITs with them without any other changes in Lean’s kernel.
There are:
- Interval .
- Pushout .
- Homotopical reals .
- (Sequential) colimit.
- Generalized circle .
- Propositional truncation as a colimit of a following sequence:
- Suspension is defined as the pushout of the span .
- Circle is the suspension of the bool .
- Sphere is the suspension of the circle .
- Join .
There are also HITs that cannot be constructed this way. These HITs are defined using standard trick with private structures.