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.
Author supplied keywords
Cite
CITATION STYLE
APA
van Doorn, F., von Raumer, J., & Buchholtz, U. (2017). Homotopy type theory in Lean. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10499 LNCS, pp. 479–495). Springer Verlag. https://doi.org/10.1007/978-3-319-66107-0_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free