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.
- groupoid/cubical — Groupoid Infinity cubical base library for cubicaltt type checker.
- groupoid/hopf — Hopf Fibrations for cubicaltt type checker.
- groupoid/infinity — cubical syntax.
- mortberg/cubicaltt — cubical type checker (Haskell) with recursive HITs.
- mortberg/yacctt — cartesian cubical type checker (Haskell).
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 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.
- RedPRL/RedPRL — PRL-family proof assistant (Standard ML).
- RedPRL/redtt — cartesian cubical type checker (OCaml).