2015-03-05 02:06:39 +00:00
|
|
|
The Lean Homotopy Type Theory Library
|
|
|
|
|
=====================================
|
|
|
|
|
|
|
|
|
|
The Lean homotopy type theory library is contained in the following
|
|
|
|
|
modules and directories:
|
|
|
|
|
|
|
|
|
|
* [init](init/init.md) : constants and theorems needed for low-level system operations
|
|
|
|
|
* [types](types/types.md) : concrete datatypes and type constructors
|
2015-04-25 00:13:08 +00:00
|
|
|
* [hit](hit/hit.md): higher inductive types
|
2015-03-05 02:06:39 +00:00
|
|
|
* [algebra](algebra/algebra.md) : algebraic structures
|
2015-04-10 22:15:47 +00:00
|
|
|
* [cubical](cubical/cubical.md) : implementation of ideas from cubical type theory
|
2015-05-01 03:26:55 +00:00
|
|
|
* [arity](arity.hlean) : a file containing theorems about functions with arity 2 or higher
|
2015-04-25 00:13:08 +00:00
|
|
|
|
2015-03-05 02:06:39 +00:00
|
|
|
Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with:
|
|
|
|
|
|
|
|
|
|
* universe polymorphism
|
2015-04-25 00:13:08 +00:00
|
|
|
* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ...
|
2015-03-05 02:06:39 +00:00
|
|
|
* inductively defined types
|
|
|
|
|
|
2015-04-10 02:14:19 +00:00
|
|
|
Note that there is no proof-irrelevant or impredicative universe.
|
|
|
|
|
|
2015-03-05 02:06:39 +00:00
|
|
|
By default, the univalence axiom is declared on initialization.
|
|
|
|
|
|
|
|
|
|
See also the [standard library](../library/library.md).
|
