nLab
Lean

Contents

Context

Constructivism, Realizability, Computability

Type theory

Contents

Idea

Lean is a proof assistant based on dependent type theory. Like Coq and Agda, it may be used to implement homotopy type theory.

Lean libraries for HoTT include:

and implementation in Lean is in

References

Last revised on January 8, 2019 at 11:43:29. See the history of this page for a list of all contributions to it.