Kubus
Cubical type theory, verified.
Kubus is a proof assistant in which equality is a path, univalence and higher inductive types compute, and every definition is certified by a kernel that is proven sound for a theory proven consistent in Lean.
Univalence computes
An equivalence of types gives a path between them, and transport along that path runs the equivalence. Negation is an equivalence of the booleans, so transporting true along ua of it gives false:
The circle, with winding numbers that run
The circle is a higher inductive type: a point base and a path loop from base to itself. Its universal cover sends the loop to the successor equivalence of the integers, so transport computes how often a loop winds around:
The library proves that the loops on the circle are exactly the integers. Hover over a name to see its type, click it to read its definition.
A verified kernel
Each definition is checked by a kernel whose functions return derivations in a formal specification of the theory. What it accepts is well formed by construction.
A consistency proof
A cubical-sets model in Lean validates every rule: no closed term of the empty type exists. It found seventeen bugs in earlier versions of the rules.
A real language
Implicit arguments and unification, nested pattern matching with coverage checking, higher inductive types, a REPL and a language server.
Checked documentation
Every snippet on this site is elaborated and kernel-certified when the site is built: the types you see on hover come from Kubus itself.
Learn more
- The tutorial starts from functions and paths and ends with univalence, the circle and the consistency proof.
- The library is rendered as hyperlinked source, with an index of definitions.
- Trust explains what is verified and what you need to read to believe it.