1.5 KiB
1.5 KiB
The Lean Homotopy Type Theory Library
The Lean Homotopy Type Theory library consists of the following directories:
- init : constants and theorems needed for low-level system operations
- types : concrete datatypes and type constructors
- hit: higher inductive types
- algebra : algebraic structures
- cubical: cubical types
The following files don't fit in any of the subfolders:
- hprop_trunc: in this file we prove that
is_trunc n Ais a mere proposition. We separate this from types.trunc to avoid circularity in imports. - eq2: coherence rules for the higher dimensional structure of equality
- function: embeddings, (split) surjections, retractions
- arity : equality theorems about functions with arity 2 or higher
See book.md for an overview of the sections of the HoTT book which have been covered.
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
- Two HITs:
n-truncation and quotients.
Note that there is no proof-irrelevant or impredicative universe.
By default, the univalence axiom is declared on initialization.
See also the standard library.