TY  - RPRT
TI  - The HoTT Library: A formalization of homotopy type theory in Coq
AU  - Andrej Bauer
AU  - Jason Gross
AU  - Peter LeFanu Lumsdaine
AU  - Mike Shulman
AU  - Matthieu Sozeau
AU  - Bas Spitters
PY  - 2016
UR  - https://arxiv.org/abs/1610.04591
ID  - 1610.04591
ER  -