Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters: The HoTT library: a formalization of homotopy type theory in Coq. CPP 2017: 164-172