CUBICAL

Groupoid Infinity:

cubicaltt

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.

Arend

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.

Lean

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

Agda

This is a base library for Agda in cubical mode.

Other Cubical Type Systems and Libraries:

RedPRL

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