Ground Zero

This library provides computable HITs, variation of Cubical Type Theory using them, and some other math.

HITs

All of the 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 many basic—not defined in terms of another Higher Inductive Type—HITs:

• Interval .
• Pushout .
• Homotopical reals .
• (Sequential) colimit.
• Generalized circle .
• Integers .
• Rational numbers .
• Möbius band.
• n-Simplex .

Other (defined in terms of another HITs) HITs:

• Propositional truncation is 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 .

• Filled n-simplex.

Cubical Type Theory (cubical/ directory)

In the topology functions from the interval to some type is a paths in this type. In HoTT book path type is defined as a classical inductive type with one constructor:

inductive eq {α : Sort u} (a : α) : α → Sort u
| refl : eq a

But if we define paths as , then we can use a nice syntax for paths as in cubicaltt or Arend:

@[refl] def refl {α : Sort u} (a : α) : a ⇝ a := <i> a

@[symm] def symm {α : Sort u} {a b : α} (p : a ⇝ b) : b ⇝ a :=
<i> p # −i

def funext {α : Sort u} {β : α → Sort v} {f g : Π (x : α), β x}
  (p : Π (x : α), f x ⇝ g x) : f ⇝ g :=
<i> λ x, p x # i

The same in cubicaltt:

refl (A : U) (a : A) : Path A a a = <i> a

symm (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> p @ -i

funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
       (p : (x : A) -> Path (B x) (f x) (g x)) :
       Path ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i

We can also define coe as in yacctt:

def coe.forward (π : I → Sort u) (i : I) (x : π i₀) : π i :=
interval.ind x (equiv.subst seg x) (equiv.path_over_subst eq.rfl) i

def coe (i k : I) (π : I → Sort u) : π i → π k :=
coe.forward (λ i, π i → π k) i (coe.forward π k)

And use it:

def trans {α β : Sort u} (p : α ⇝ β) : α → β :=
coe 0 1 (λ i, p # i)

def trans_neg {α β : Sort u} (p : α ⇝ β) : β → α :=
coe 1 0 (λ i, p # i)

def transK {α β : Sort u} (p : α ⇝ β) (x : α) :
  x ⇝ trans_neg p (trans p x) :=
<i> coe i 0 (λ i, p # i) (coe 0 i (λ i, p # i) x)

In yacctt:

trans (A B : U) (p : Path U A B) (a : A) : B = coe 0->1 p a
transNeg (A B : U) (p : Path U A B) (b : B) : A = coe 1->0 p b

transK (A B : U) (p : Path U A B) (a : A) :
  Path A a (transNeg A B p (trans A B p a)) =
  <i> coe i->0 p (coe 0->i p a)

We can freely transform cubical paths to classical and back:

def from_equality {α : Sort u} {a b : α} (p : a = b :> α) : Path a b :=
Path.lam (interval.rec a b p)

def to_equality {α : Sort u} {a b : α} (p : Path a b) : a = b :> α :=
begin cases p with f, apply eq.map, exact interval.seg end

Dependency map