The Lean homotopy type theory library is contained in the following modules and directories:
- init : constants and theorems needed for low-level system operations
- types : concrete datatypes and type constructors
- algebra : algebraic structures
Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with:
- universe polymorphism
- a non-cumulative hierarchy of universes,
Type 0,Type 1, ... - inductively defined types
Note that there is no proof-irrelevant or impredicative universe.
By default, the univalence axiom is declared on initialization.
See also the standard library.