mlang

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

• build & run & debug & editor setup
• roadmap
• changelog
• internals & help wanted