# nLab Lean

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# 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.