Good Fibrations through the Modal Prism

TL;DR

This paper develops a theory of modal fibrations within homotopy type theory, specifically applying it to the shape modality of Real Cohesion, to bridge the gap between abstract homotopy theory and algebraic topology.

Contribution

It introduces a general theory of modal fibrations and applies it to Real Cohesion, enabling the study of algebraic topology within homotopy type theory.

Findings

Development of a theory of modal fibrations for a general modality

Application of modal fibrations to the shape modality of Real Cohesion

Examples of modal fibrations and the theory of covering spaces in Real Cohesive HoTT

Abstract

Homotopy type theory is a formal language for doing abstract homotopy theory -- the study of identifications. But in unmodified homotopy type theory, there is no way to say that these identifications come from identifying the path-connected points of a space. In other words, we can do abstract homotopy theory, but not algebraic topology. Shulman's Real Cohesive HoTT remedies this issue by introducing a system of modalities that relate the spatial structure of types to their homotopical structure. In this paper, we develop a theory of modal fibrations for a general modality, and apply it in particular to the shape modality of Real Cohesion. We then give examples of modal fibrations in Real Cohesive HoTT, and develop the theory of covering spaces.