···

       
141
       
 
       
\end{equation}

     

       
142
       
 
       
from which it follows that the boundary inclusion $\{0\}+\{1\}\hookrightarrow \mathbb{I}$ is an equivalence and hence that all synthetic spaces are codiscrete.

     

       
143
       
 
       


     

       
144
       
-
       
When a dependent type theorist working in a topos $\mathcal{S}$ says \emph{``Let $X$ be a type\ldots''}, what follows is in some sense taking place not in $\mathcal{S}$ but in the classifying topos $\mathcal{S}[X]$ of an object over $\mathcal{S}$. So an assumed type is, in the dependent type theoretic interpretation, a \emph{generic} type rather than an \emph{arbitrary} type.  In contrast, a practitioner of the Mitchell--B\'enabou language of toposes would explain the same turn of phrase as a conservative use of \emph{prenex polymorphism} over simple type theory; a schema of this kind can only be instantiated with a global type, and so the bad deduction \eqref{bad-deduction} would not obtain.

     

       
145
       
 
       


     

       
146
       
 
       
Those who do not wish to sacrifice all the advantages of dependent type theory may instead introduce \emph{modalities} that can be used to safely state assumptions that are meant to hold only globally. These modalities do come at a cost, but they have proved indispensible to prior work in the general development of synthetic higher category theory inside dependent type theory~\citep{11186122}.

     

       
147
       
 
       


     

···

       
141
       
 
       
\end{equation}

     

       
142
       
 
       
from which it follows that the boundary inclusion $\{0\}+\{1\}\hookrightarrow \mathbb{I}$ is an equivalence and hence that all synthetic spaces are codiscrete.

     

       
143
       
 
       


     

       
144
       
+
       
When a dependent type theorist working internally to a category $\mathcal{S}$ says \emph{``Let $X$ be a type\ldots''}, what follows is taking place not in $\mathcal{S}$ but in the free extension $\mathcal{S}[X]$ of $\mathcal{S}$ by an object. So an assumed type is, in the dependent type theoretic interpretation, a \emph{generic} type rather than an \emph{arbitrary} type.  In contrast, a practitioner of the Mitchell--B\'enabou language of toposes would explain the same turn of phrase as a conservative use of \emph{prenex polymorphism} over simple type theory; a schema of this kind can only be instantiated with a global type, and so the bad deduction \eqref{bad-deduction} would not obtain.

     

       
145
       
 
       


     

       
146
       
 
       
Those who do not wish to sacrifice all the advantages of dependent type theory may instead introduce \emph{modalities} that can be used to safely state assumptions that are meant to hold only globally. These modalities do come at a cost, but they have proved indispensible to prior work in the general development of synthetic higher category theory inside dependent type theory~\citep{11186122}.

     

       
147