The HoTT Library: A formalization of homotopy type theory in Coq

arXiv1610.04591MaRDI QIDQ6278647

Andrej Bauer, Bas Spitters, Peter LeFanu Lumsdaine, Matthieu Sozeau, Jason Gross, Mike Shulman

Publication date: 14 October 2016

Mathematics Subject Classification ID

Logic in computer science (03B70) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

This page was built for publication: The HoTT Library: A formalization of homotopy type theory in Coq