Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters. The HoTT library: a formalization of homotopy type theory in Coq. In Yves Bertot, Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pages 164-172, ACM, 2017. [doi]
Abstract is missing.