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.

A morphism of categories with \(U\)-étale morphisms is a structure-preserving functor. Note that preservation of universal étale morphism is a proposition because of univalence.