- -\(U\)-logos → [0004]
- -\(U\)-topos → [0005]
- -base type theory → [0023]
- -\(I\)-categorically fibrant object → [0032]
- -categorically fibrant type → [0059]
- -category with \(U\)-étale morphisms → [001M]
- -coétale point → [003U]
- -constant sheaf → [003K]
- -coproduct → [0026]
- -descent → [004X]
- -direct image → [003L]
- -directed univalence → [005D]
- -\(V\)-enlargement → [001E]
- -essential morphism → [003P]
- -essential point → [003Q]
- -étale colimit → [0017]
- -étale limit → [0017]
- -étale morphism
in a category with \(U\)-étale morphisms. → [001M]
- -étale morphism of toposes → [000N]
- -étale morphism of lex \(U\)-cocomplete categories → [000V]
- -étale type → [002A]
- -finitely presented point → [003Z]
- -global section → [003K]
- -global section translation → [002P]
- -globalization → [002T]
- -inverse image → [000O]
- -inverse image → [003I]
- -left fibration → [005B]
- -\(I\)-left fibration → [005A]
- -lex \(U\)-cocomplete category → [0001]
- -model → [003C]
- -morphism of lex \(U\)-cocomplete categories → [0002]
- -\(U\)-presentable category → [004Y]
- -\((U,\kappa )\)-presentable category → [004Y]
- -product → [0025]
- -self-internalization of \(T\) → [002N]
- -sheaf → [003B]
- -sheaf on \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\) → [0016]
- -slice type theory → [002U]
- -standard \(n\)-simplex → [0049]
- -subtopos → [004H]
- -topos → [0052]
- -topos of linear order → [0043]
- -topos of propositions → [004N]
- -topos of types → [003W]
- -universal étale morphism
in a category with \(U\)-étale morphisms. → [001M]