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.
- logic
You can import the core part of the library by writing import core
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. We port some files from the standard library to the HoTT library.