Konferenzartikel: Homotopy Type Theory in Lean

[DBLP:conf/itp/DoornRB17]

Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz, Homotopy Type Theory in Lean, Mauricio Ayala{-}Rinc{\'O}n and C{\'E}sar A. Mu{\~N}oz (Ed.), Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings, pp. 479--495, Springer, 2017.

Zusammenfassung

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.

Download

[DOI]

Original article available at springerlink.com.

BibTeX

@inproceedings{DBLP:conf/itp/DoornRB17,
  title = {Homotopy Type Theory in Lean},
  booktitle = {Interactive Theorem Proving - 8th International Conference, ITP
        2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
  year = {2017},
  publisher = {Springer},
  volume = {10499},
  pages = {479--495},
  author = {Floris van Doorn and Jakob von Raumer and Ulrik Buchholtz},
  editor = {Mauricio Ayala{-}Rinc{\'O}n and
        C{\'E}sar A. Mu{\~N}oz},
  series = {Lecture Notes in Computer Science},
  url = {https://doi.org/10.1007/978-3-319-66107-0\\_30},
  doi = {10.1007/978-3-319-66107-0\_30},
}

Institutsinterne Autoren

Wissenschaftliche Mitarbeiter
Dr. Jakob von Raumer