Characterizations of modalities and lex modalities (Q2229967)

\textit{Homotopy type theory} [\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)] is a formal system which has models in all \(\infty\)-toposes [\textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, Adv. Math. 337, 1--38 (2018; Zbl 1397.18015); \textit{P. L. Lumsdaine} and \textit{M. Shulman}, Math. Proc. Camb. Philos. Soc. 169, No. 1, 159--208 (2020; Zbl 1470.18007); \textit{M. Shulman}, ``All $(\infty,1)$-toposes have strict univalent universes'', Preprint, \url{arXiv:1904.07004}]. The notion of a \textit{reflective universe} in homotopy type theory simultaneously encodes the idea of localization of an \(\infty\)-topos and common modalities studied in logic [\textit{D. Corfield}, Modal homotopy type theory. The prospect of a new logic for philosophy. Oxford: Oxford University Press (2020; Zbl 1436.00033)]. All of the results in this paper are stated and established within the framework of homotopy type theory, so that similar results hold in any \(\infty\)-topos. A universe \(\mathcal{U}\) is fixed. A reflective subuniverse \(L\) consists of a subuniverse \[ \text{is-local}_{L}:\mathcal{U}\rightarrow\mathrm{Prop} \] a function \[ L:\mathcal{U}\rightarrow\mathcal{U} \] and a \textit{localization} (called the \textit{unit} map) \[ \eta_{X}:X\rightarrow LX \] for each \(X:\mathcal{U}\). The operation is functorial in the sense that, for any map \(f:X\rightarrow Y\), there is a unique map \(L_f:LX\rightarrow LY\) making the square (called the \(L\)\textit{-naturality square}) \[ \begin{array} [c]{ccc} X & \overset{\eta}{\rightarrow} & LX\\ {}_{f}\downarrow & & \downarrow{}_{L_f}\\ Y & \underset{\eta}{\rightarrow} & LY \end{array} \] commutative. A map \(f\) is said to be \begin{itemize} \item \(L\)\textit{-local} if its fibers are \(L\)-local, \item \(L\)\textit{-étale} if its \(L\)-naturality square is a pullback square, \item \(L\)\textit{-connected} if it fibers are \(L\)-connected, and \item an \(L\)\textit{-equivalence} if \(L_f\) is an equivalence. \end{itemize} A reflective subuniverse is called a \textit{modality} if for any family \(P\) of \(L\)-local types over an \(L\)-local type \(X\), the dependent sum \[ \sum\nolimits_{(x:X)}P(x) \] is again \(L\)-local, that is to say, if the \(L\)-local types are \(\sum\)-closed. A reflective subuniverse \(L\) is said to be \textit{left exact} or \textit{lex} for short if the operation \(L\) preserves pullbacks. A \textit{class of maps} means a subtype \[ \sum\nolimits_{(x:X:\mathcal{U})}Y^{X} \] defined by a predicate valued in \(\mathrm{Prop}\). A class of maps \(\mathcal{L}\) is said to be \textit{left orthogoanl} to a class of maps \(\mathcal{R}\), and \(\mathcal{R}\) is said to be \textit{right orthogonal} to \(\mathcal{L}\) if, for every \(f:A\rightarrow B\) in \(\mathcal{L}\) and for every \(g:X\rightarrow Y\) in \(\mathcal{R}\), the square \[ \begin{array} [c]{ccc} X^{B} & \overset{f^{\ast}}{\rightarrow} & X^{A}\\ {}_{g_{\ast}}\downarrow & & \downarrow{}_{g_{\ast}}\\ Y^{B} & \underset{f^{+}}{\rightarrow} & Y^{A} \end{array} \] is a pullback. For any class of maps \(\mathcal{M}\), \(\mathcal{M}^{\bot}\) denotes the class of maps that are right orthogonal to \(\mathcal{M}\), while \(^{\bot}\mathcal{M}\) denotes the class of maps that are left orthogonal to \(\mathcal{M}\). An \textit{orthogonal factorization system} on \(\mathcal{U}\) is a pair \((\mathcal{L},\mathcal{R})\) of classes of maps in \(\mathcal{U}\) such that \(\mathcal{L}=^{\bot}\mathcal{R}\), \(\mathcal{R}=\mathcal{L}^{\bot }\), and every map \(h:X\rightarrow Y\) factors as a left map followed by a right map. Every modality gives rise to two orthogonal factorization systems. \begin{itemize} \item The \textit{stable factorization system} in which the left class \(\mathcal{L}\) consists of the \(L\)-connected maps, and the right class \(\mathcal{R}\) consists of the \(L\)-local maps \item The \textit{reflective factorization system} in which the left class \(\mathcal{L}\) consists of the \(L\)-equivalences, and the right class \(\mathcal{R}\) consists of the \(L\)-étale maps \end{itemize} However, both of these pairs of classes of maps fail to be orthogonal factorization systems in the more general case of a reflective subunivers. This paper addresses a thorough understanding of how these four classes of maps relate. A type \(X\) is said to be \(L\)\textit{-separated} if its identity types are \(L\)-local. It was shown in [\textit{J. D. Christensen} et al., High. Struct. 4, No. 1, 1--32 (2020; Zbl 1439.18023)] that the subuniverse of \(L\)-separated types is again a reflective subuniverse, which is denoted by \(L^{^{\prime}}\). A reflective subuniverse is said to be \textit{accessible} if it can be presented as the subuniverse of \(f\)-local types, for a family of maps \(\left\{ f_{i}:A_{i}\rightarrow B_{i}\right\}\) in \(\mathcal{U}\), indexed by a type \(I\) in \(\mathcal{U}\), where a type is said to be \(f\)\textit{-local} if the precomposition map \[ f_{i}^{\ast}:(B_{i}\rightarrow X)\rightarrow(A_{i}\rightarrow X) \] is an equivalence for each \(i:I\). For any family of maps \(f\) in \(\mathcal{U}\), the subuniverse of \(f\)-local types is a reflective subuniverse, which is a modality provided that each \(B_{i}\) is contractible, in which the modal operator \(X\mapsto LX\) is called \textit{nullification}. The principal result is the following omnibus theorem. Theorem. In the following diagram \[\begin{aligned} & \begin{array} [c]{ccccccccc} & & & & & & & & ^{\bot}\left\{ L^{\prime}\text{-étale maps}\right\} \\ & & & & & & & & \downarrow_{i_{6}}\\ ^{\bot}\left\{ L\text{-étale maps}\right\} & \overset{i_{1}}{=} & \left\{ L\text{-equivalences}\right\} & \overset{i_{2}}{\leftarrow} & ^{\bot}(\left\{ f_{i}\right\} ^{\bot})& \overset{i_{3}}{\leftarrow} & ^{\bot}(\left\{ \eta_{X}\right\} ^{\bot})& \overset{i_{4}}{\leftarrow} & ^{\bot}\left\{ L\text{-local maps}\right\} \\ \left\{ L\text{-étale maps}\right\} & \underset{j_{1}}{\rightarrow} & \left\{ L\text{-equivalences}\right\} ^{\bot} & \underset{j_{2}}{\rightarrow} & \left\{ f_{i}\right\} ^{\bot} & \underset{j_{3}}{\rightarrow} & \left\{ \eta_{X}\right\} ^{\bot} & \underset{j_{4}}{\rightarrow} & \left\{ L\text{-connected maps}\right\} ^{\bot}\\ & & & & & & & & \underset{\downarrow}{\overset{}{\vdots}}_{j_{6}}\\ & & & & & & & & \left\{ L^{\prime}\text{-étale maps}\right\} \end{array} \\ & \begin{array} [c]{ccc} \overset{i_{8}}{=} & \left\{ L^{\prime}\text{-equivalences}\right\} & \cdots\\ & \downarrow_{i_{7}} & \\ \overset{i_{5}}{=} & \left\{ L\text{-connected maps}\right\} & \\ \underset{j_{5}}{\rightarrow} & \left\{ L\text{-connected maps}\right\}^{\bot} & \\ & \downarrow_{j_{7}} & \\ \underset{j_{8}}{\rightarrow} & \left\{ L^{\prime}\text{-equivalences}\right\} ^{\bot} & \cdots \end{array} \end{aligned} \] where \begin{itemize} \item the arrows should be interpreted as implications between propositions; \item the column concerning the family of maps \(\left\{ f_{i}\right\}\) only applies if the reflective subuniverse is presented by \(\left\{ f_{i}\right\}\), the composites \(i_{2}\circ i_{3}\) and \(j_{3}\circ j_{2}\) apply in general; \item the diagram continues infinitely to the right, with \(L\) replaced by \(L^{\prime}\), the family \(\left\{ f_{i}\right\}\) replaced by the family \(\left\{ \sum f_{i}\right\}\) of suspensions, and the subscripts increased by \(7\) in each subsequent row; \item every arrow is an inclusion. \end{itemize} We have the following eight statements. \begin{itemize} \item[1.] The equalities \(i_{1+7n}\) and \(i_{5+7n}\) hold, so that each class on the upper is obtained from its mirror image class on the lower by applying \(^{\bot}(-)\). \item[2.] All of the inclusions, except possibly the inclusion \(j_{6+7n}\) hold. \item[3.] The following are equivalent: \begin{itemize} \item[(i)] \(L^{\prime}\) is a modality. \item[(ii)] The inclusion \(j_{8}\) is an equility. \item[(iii)] The inclusion \(j_{6}\) exists. \end{itemize} \item[4.] The following are equivalent: \begin{itemize} \item[(i)] \(L\) is a modality. \item[(ii)] The inclusion \(i_{4}\) is an equility. \item[(iii)] The inclusion \(j_{4}\) is an equility. \item[(iv)] The inclusion \(j_{5}\) is an equility. \end{itemize} Also, when \(L\) is a lex modality, \(j_{1}\) is an equality and the equivalent conditions in 7 hold. If, in addition, \(L\) is presented as a nullification, then \(i_{3}\) and \(j_{3}\) are equalities. \item[5.] The following are equivalent: \begin{itemize} \item[(i)] \(L\) is a lex modality. \item[(ii)] \(L\) is a lex reflective subuniverse. \item[(iii)] All of the displayed horizontal inclusions are equalities. \item[(iv)] The inclusion \(j_{4}\circ\cdots\circ j_{1}\) is an equality. \item[(v)] The inclusion \(j_{4}\circ j_{3}\circ j_{2}\) is an equality. \item[(vi)] The inclusion \(i_{4}\circ i_{3}\circ i_{2}\) is an equality \end{itemize} Also, when \(L\) is a lex modality, the equivalent conditions in 8 hold. \item[6.] The following are equivalent: \begin{itemize} \item[(i)] \(L=L^{\prime}\). \item[(ii)] All of the inclusions are equalities, including those not displayed. \item[(iii)] Every \(L^{\prime}\)-étale map is \(L\)-local. \item[(iv)] \(L\) is cotopological. \item[(v)] \(L\) is lex and every unit \(\eta\) is surjective. \item[(vi)] \(L\) is lex and every mere propositio is \(L\)-local. \end{itemize} Also, when \(L=L^{\prime}\), the equivalent conditions in 9 hold. \item[7.] For each of the inclusions not drawn as equalities, including \(j_{6}\) and those not displayed, there exists an accessible reflective subuniverse \(L\) making the inclusion strict. \item[8.] In general, neither of \(\left\{ L\text{-connected maps}\right\} ^{\bot}\) and \(\left\{ L^{\prime}\text{-étale maps}\right\}\) is included in the other. \end{itemize} This paper is largely devoted to the proof of the above theorem. The \(n\)-truncation modality is addressed in \S 2, \S 4, \S 5 and \S 7.