A cubical type theory implementation. features you might not found in Coq, Agda, Lean:
- structural record and sum types
- overlapping patterns, so you don't need a lemma to proof nat_plus_commutative
- cumulative universe with lift operator and universe/pi subtyping
see roadmap for details.
see library and tests folder for sample code. for example Brunerie Number