HOME | DEUTSCH | IMPRESSUM | KIT

Conference Papers: 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.

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.

Download

  [DOI]

Original article available at springerlink.com.

BibTeX

Authors at the institute

Scientific Staff
Dr. Jakob von Raumer