论文标题
模态下降
Modal Descent
论文作者
论文摘要
同型类型理论中的任何模态都会引起正交分解系统，在该系统下，左类在回调下是稳定的。我们表明，与任何模态相关的第二个正交分解系统，其中左类是$ \ bigcirc $ - 等效的类，正确的类是$ \ bigcirc $-étale地图的类。这种分解系统称为模态的反射分解系统，我们对形式的反射分解系统的正交分解系统进行了精确表征。在$ n $ truncation的特殊情况下，反射分解系统具有一个简单的描述：我们证明$ n $-étale地图是地图$ \ m athbf {1} \ to \ mathbf {s}^{s}^{n+1} $。我们使用$ \ bigCirc $-étale地图来证明模态下降定理：带有模纤维的地图中$ \ bigcirc x $与$ \ bigcirc $-étale地图与$ x $的$ \ bigcirc $ - étale地图是同一件事。我们以对实现同型类型理论的应用程序进行了结论，并指出了$ \ bigCirc $-étale地图与代数几何形状的正式依托图有关。
Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated to any modality, of which the left class is the class of $\bigcirc$-equivalences and the right class is the class of $\bigcirc$-étale maps. This factorization system is called the reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the reflective factorization system of a modality. In the special case of the $n$-truncation the reflective factorization system has a simple description: we show that the $n$-étale maps are the maps that are right orthogonal to the map $\mathbf{1} \to \mathbf{S}^{n+1}$. We use the $\bigcirc$-étale maps to prove a modal descent theorem: a map with modal fibers into $\bigcirc X$ is the same thing as a $\bigcirc$-étale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remarks how $\bigcirc$-étale maps relate to the formally etale maps from algebraic geometry.
