一句话：系统建立同伦类型论中的因子分解系统、反射子宇宙与模态理论，并用局部化高阶归纳类型构造它们。
本文研究单价同伦类型论（HoTT）中的模态理论。HoTT 可视为 ∞-群胚范畴的语言，并作为数学新基础及高阶拓扑斯的内部语言。作者发展了因子分解系统、反射子宇宙与模态的一般理论，引入“局部化”高阶归纳类型来构造模态，由此得到 (n-连通, n-截断) 因子分解系统以及通过 lex 模态对子拓扑斯的内部表示。文中还建立了这些构造的语义解释，说明它们如何对应高阶拓扑斯中的相应结构。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{RijkeSS17,
title = {Modalities in homotopy type theory},
author = {Egbert Rijke and Michael Shulman and Bas Spitters},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:2)2020}
}