Groupoid Infinity Language Nucleus Experiments:


CCHM/HTS Homotopy Type System with Strict Equality.

Smiling Buddha

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

Castle Bravo

Cubical type checker with definitional β-rule for Path types which allows us to avoid separate Id type like in cubicaltt. Computable winding.

Ivy Mike

Arend is a cartesian cubical type checker by JetBrains that supports HITs, extensible records, type classes, implicit variables. It also contains Agda-style reasoning library.

Ground Zero

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


This is a base library for Agda in cubical mode.

Other Cubical Type Systems and Libraries:


The redtt is a cartesian cubical type checker that take its roots from RedPRL and JonPRL.