Modalities in homotopy type theory

Egbert Rijke, Michael Shulman, Bas Spitters

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal…