☰
Synthetic topos theory
Introduction
Structure
Status
Logoses and toposes
Étale morphisms
A universal property of
\(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\)
Sheaves on
\(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\)
Internal topos theory
Topical type theory
Universe levels
Core type theory
Base type theory
Internal type theories
Type theory of spaces
Type theory of sheaves
Cross-theory axioms
Topos theory
Classifying spaces
The category of sheaves
Inverse images
Direct images
Étale toposes
Essential morphisms
Subtoposes and modalities
The topos of types
The topos of propositions
Linear orders and simplicial types
Index
Notation index
Bibliography
[index]
[0039]
[0039]
Topos theory
We develop basic topos theory in the topical type theory.
Classifying spaces
The category of sheaves
Inverse images
Direct images
Étale toposes
Essential morphisms
Subtoposes and modalities
←
↑
→