TY  - RPRT
TI  - Homotopy Type Theory in Lean
AU  - Floris van Doorn
AU  - Jakob von Raumer
AU  - Ulrik Buchholtz
PY  - 2017
DO  - 10.1007/978-3-319-66107-0_30
UR  - https://arxiv.org/abs/1704.06781
ID  - 1704.06781
ER  -