  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.
