[001L] A universal property of $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$

Let $U$ be a universe. A category with $U$-étale morphisms $C$ consists of the following data.

• -A category $C.\mathord {\textnormal {\textsf {Carrier}}}$ with $U$-small limits.
• -A univalent morphism $C.\mathord {\textnormal {\textsf {p}}}:C.\mathbb {A}_{\bullet }\rightarrow C.\mathbb {A}$ in $C.\mathord {\textnormal {\textsf {Carrier}}}$ called the universal étale morphism. Pullbacks of $C.\mathord {\textnormal {\textsf {p}}}$ are called étale morphisms. For an object $x:C.\mathord {\textnormal {\textsf {Carrier}}}$, let $\mathord {\textnormal {\textsf {Etale}}}(x)$ denote the full subcategory of $C.\mathord {\textnormal {\textsf {Carrier}}}/x$ spanned by the étale morphisms with codomain $x$.
• -All the identity morphisms in $C.\mathord {\textnormal {\textsf {Carrier}}}$ are étale, étale morphisms are closed under composition, and étale morphisms are closed under diagonal.
• -For every object $x:C.\mathord {\textnormal {\textsf {Carrier}}}$, the category $\mathord {\textnormal {\textsf {Etale}}}(x)$ has $U$-small colimits preserved by the inclusion $\mathord {\textnormal {\textsf {Etale}}}(x)\rightarrow C.\mathord {\textnormal {\textsf {Carrier}}}/x$.
• -For every morphism $f:x\rightarrow y$ in $C.\mathord {\textnormal {\textsf {Carrier}}}$, the pullback functor ${f}^{*}:\mathord {\textnormal {\textsf {Etale}}}(y)\rightarrow \mathord {\textnormal {\textsf {Etale}}}(x)$ preserves $U$-small colimits.
• -$C.\mathord {\textnormal {\textsf {p}}}$ is exponentiable.

Let $U$ be a universe. Then $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ is the initial category with $U$-étale morphisms, where the universal étale morphism in $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ is $\mathord {\textnormal {\textsf {p}}}:\mathbb {A}_{\bullet }\rightarrow \mathbb {A}$ defined in [000K].