Homotopy Type Theory in Lean
classification
💻 cs.LO
math.LO
keywords
homotopytheoryleanlibrarytypeassistantcubicaldiscuss
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.