Groupoid Infinity Language Nucleus Experiments:

Smiling Buddha

The cubicaltt is a cubical CCHM type checker (Mörtberg) that supports path interval, connections, homogeneous compositions and generalized transport, higher inductive types, gluening of types and values. Recursive HITs have complete support only in hcomp version.


Homotopy Type System (Voevodsky) with Strict Equality and CCHM Agda primitives.

Castle Bravo

Cubical type checker of HoTT-∂ Type System (Siegment) with definitional β-rule for Path types which allows us to avoid separate Id type like in cubicaltt. Computable winding.


Cubical type checker of HoTT-I Type System (Valery Isaev) with definitional β-rule for Path types.

Ground Zero

Ground Zero is a cubical model and cubical base library embedded into Lean.