lean2/hott/hott.md

1.1 KiB

The Lean Homotopy Type Theory Library

The Lean homotopy type theory library is contained in the following files and directories:

  • init : constants and theorems needed for low-level system operations
  • types : concrete datatypes and type constructors
  • hit: higher inductive types
  • algebra : algebraic structures
  • arity : a file containing 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.