Homotopy Type Theory in Lean
Logic in Computer Science
2017-09-21 v2 Logic
Abstract
We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.
Keywords
Cite
@article{arxiv.1704.06781,
title = {Homotopy Type Theory in Lean},
author = {Floris van Doorn and Jakob von Raumer and Ulrik Buchholtz},
journal= {arXiv preprint arXiv:1704.06781},
year = {2017}
}
Comments
17 pages, accepted for ITP 2017