Tutorial
From functions and paths to univalence, the circle and the kernel. Every example is checked by Kubus when this site is built: hover over names to see their types, click to jump to definitions; a ✓ marks declarations certified by the kernel.
- What Kubus is
- Getting started
- Functions, pairs and implicit arguments
- The interval and paths
- Composition
- Transport and path induction
- Data types and recursion
- Equivalences, Glue and univalence
- Higher inductive types
- Universes and displacement
- Trust: the kernel and the consistency proof
- Reference
Kubus