论文标题
模式和LEX方式的特征
Characterizations of modalities and lex modalities
论文作者
论文摘要
同型类型理论中的反思性子名称是拓扑结构或$ \ infty $ - 类别理论的内部版本。在同型类型理论方面，我们在反思性subuniverse $ l $中给出了以下条件的新特征：（1）相关的subuniverse $ l'$ of $ l $ l $分隔类型是一种方式； （2）$ l $是一种方式； （3）$ l $是Lex模式； （4）$ l $是一种创作方式。在每种情况下，我们都会提供几个必要和充分的条件。我们的特征涉及与$ l $相关的各种地图家族，例如$ l $ - Étale地图，$ l $ - 等价率，$ l $ local-local Maps，$ l $连接的地图，单位地图$η_x$，以及他们的左和/或左和/或右Orthogonal Effpersements。更一般而言，我们的主要定理概述了所有这些类别如何相互关联。我们还举例说明，这些图表之间我们描述的所有夹杂物都可能严格。
A reflective subuniverse in homotopy type theory is an internal version of the notion of a localization in topology or in the theory of $\infty$-categories. Working in homotopy type theory, we give new characterizations of the following conditions on a reflective subuniverse $L$: (1) the associated subuniverse $L'$ of $L$-separated types is a modality; (2) $L$ is a modality; (3) $L$ is a lex modality; and (4) $L$ is a cotopological modality. In each case, we give several necessary and sufficient conditions. Our characterizations involve various families of maps associated to $L$, such as the $L$-étale maps, the $L$-equivalences, the $L$-local maps, the $L$-connected maps, the unit maps $η_X$, and their left and/or right orthogonal complements. More generally, our main theorem gives an overview of how all of these classes related to each other. We also give examples that show that all of the inclusions we describe between these classes of maps can be strict.
