The Lean Homotopy Type Theory Library
The Lean Homotopy Type Theory library consists of the following directories:
- init : basic definitions and theorems. These are imported in each ".hlean" file by default, unless the
preludecommand is used.
- types : concrete datatypes and type constructors
- algebra : algebraic structures, group theory and category theory.
- cubical : cubical types (e.g. squares in a types, squareovers)
- hit: higher inductive types. Some higher inductive types which are mostly relevant in homotopy theory are in the homotopy folder.
- homotopy : synthetic homotopy theory.
The following files don't fit in any of the subfolders:
- prop_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
- choice : theorems about the axiom of choice.
You can import the core part of the library by writing
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 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.