-Category theory ( ∞ , 1 ) (\infty,1)
(∞,1)-category theory Background
-Topos Theory ( ∞ , 1 ) (\infty,1)
(∞,1)-topos theory Background
(∞,1)-category of (∞,1)-sheaves
Extra stuff, structure and property
locally n-connected (n,1)-topos
locally ∞-connected (∞,1)-topos, ∞-connected (∞,1)-topos
cohesive (∞,1)-topos Models
structures in a cohesive (∞,1)-topos Contents
The notion of an
elementary (∞,1)-topos is the analog of the notion of in elementary topos (∞,1)-category theory.
This is in contrast to the notion of an
, the analog of a (∞,1)-topos equivalent to an (∞,1)-category of (∞,1)-sheaves sheaf topos, which is more specific (see geometric homotopy type theory).
(∞,1)-sheaf (∞,1)-topos provides categorical semantics for homotopy type theory with a univalent Tarskian- type of types (and higher inductive types), one idea is roughly that elementary -topos should be defined as the larger class which is exactly the ( ∞ , 1 ) (\infty,1) categorical semantics for homotopy type theory in this sense. For more on this see at References
A proposal for a definition, with an eye towards
homotopy type theory and the relation between type theory and category theory is on the very last slide of
This proposal is
predicative, but could be made impredicative easily (to correspond closer to elementary 1-toposes rather than to types of 1- pretoposes) by adding a subobject classifier (i.e. a classifier for all subobjects, rather than merely the “classifiers for small subobjects” obtainable from object classifiers).
Related discussion is in
See maybe also the comments at