_Modalities in homotopy type theory_. [[Egbert Rijke]], [[Michael Shulman]], [[Bas Spitters]]. ## Links ## [arXiv:1706.07526](https://arxiv.org/abs/1706.07526) ### Abstract ### 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 language for (elementary) higher toposes. We develop the theory of [[factorization systems]], [[reflective subuniverses]], and [[modalities]] in homotopy type theory, including their construction using a "[[localization]]" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions. ## See also ## * [[Localization in Homotopy Type Theory]] * [[References]] category: reference