Homotopy limits in type theory

TL;DR

This paper explores homotopy limits within homotopy type theory, formalizing the concepts in Coq and comparing them to classical methods, addressing challenges in formalization.

Contribution

It provides a systematic formalization of homotopy limits in type theory and compares it with classical approaches, advancing formal methods in homotopy theory.

Findings

Successfully formalized homotopy limits in Coq

Identified challenges in formalizing homotopy-theoretic concepts

Compared type-theoretic and classical approaches to homotopy limits

Abstract

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.