137 citations · 500 across the 20 of their papers we have counts for
4 papers · 1 filter
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including un…
The homotopy theory of type theories
Chris Kapulkin, Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on ). This presents an -category of su…
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Kuen-Bang Hou, Eric Finster, Dan Licata +1
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present…
Constructive reflectivity principles for regular theories
Henrik Forssell, Peter LeFanu Lumsdaine
Classically, any structure for a signature may be completed to a model of a desired regular theory by means of the chase construction or small object argument. Moreover, th…