Reseña: Homotopy limits in Coq

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Homotopy limits in Coq.

Sus autores son Jeremy Avigad (de la Carnegie Mellon University), Krzysztof Kapulkin (de la Univ. de Pittsburgh) y Peter LeFanu Lumsdaine.

Su resumen es

Working in Homotopy Type Theory, we provide a systematic study of basic homotopy limits and related constructions. The entire development has been formally verified in the Coq interactive proof assistant.

Las teorías en Coq correspondientes al artículo se encuentra aquí.