Synthetic topos theory

[term-index] Index

  • -\(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]