Connectedness through decidable quotients (Q6945780)

\textit{C. McLarty} [J. Philos. Log. 17, No. 1, 75--90 (1988; Zbl 0652.03038)] formalizes a development of the notion of set out of space through topos theory, considering the following two postulates.\N\N\begin{itemize}\N\item[(NS)] Any object is either initial or has a global element.\N\N\item[(DSO)] There exists a unique decidable subobject for any given object containing all of its points.\N\end{itemize}\N\NThis paper considers the following postulate too.\N\N\begin{itemize}\N\item[(DQO)] There exists a unique decidable quotient for any given object along with any arrow to 2 factors uniquely.\N\end{itemize}\N\NIn the presence of DQO, let\N\[\Np_{X}:X\rightarrow\Pi\left( X\right)\N\]\Nbe the corresponding quotient map. The first main result claims that\N\NTheorem. For a topos \(\mathcal{E}\)\ abiding by NS and DQO, \ is the object part of a finite-product-preserving functor left adjoint to the inclusion of \(\mathrm{Dec}\left( \mathcal{E}\right) \).\N\NIt is shown in \S 2.3 that\N\NTheorem. For a topos \(\mathcal{E}\)\ satisfying NS, \(\mathrm{Dec}\left( \mathcal{E} \right) \)\ is an exponential ideal as soon as it is reflective.\N\NIt is shown in \S 3 that\N\NTheorem. Let \(\mathcal{E}\)\ be a topos abiding by NS. Then \(\mathcal{E}\)\ satisfies DQO and McLarty's DSO iff \(\mathcal{E}\)\ is precohesive over \(\mathrm{Dec}\left( \mathcal{E}\right) \).\N\NIn an extensive category, an object is connected if it has exactly two complemented subobjects. On the other hand, \textit{F. W. Lawvere} [Theory Appl. Categ. 19, 41--49 (2007; Zbl 1123.18001)] calls an object connected in the context of precohesion if its image under the left-most adjoint is terminal. It is shown in \S 1.1 that in the presence of NS and DQO both agree. Therefore the authors argue that the addition of DQO is a natural extension of McLarty's axioms for SDG that frames it in a context of Lawvere's precohesion.