nLab
elementary (infinity,1)-topos
Context
$(\infty,1)$ -Category theory
(∞,1)-category theory

Background
Basic concepts
Universal constructions
Local presentation
Theorems
Models
$(\infty,1)$ -Topos Theory
(∞,1)-topos theory

Background
Definitions
elementary (∞,1)-topos

(∞,1)-site

reflective sub-(∞,1)-category

(∞,1)-category of (∞,1)-sheaves

(∞,1)-topos

(n,1)-topos , n-topos

(∞,1)-quasitopos

(∞,2)-topos

(∞,n)-topos

Characterization
Morphisms
Extra stuff, structure and property
hypercomplete (∞,1)-topos

over-(∞,1)-topos

n-localic (∞,1)-topos

locally n-connected (n,1)-topos

structured (∞,1)-topos

locally ∞-connected (∞,1)-topos , ∞-connected (∞,1)-topos

local (∞,1)-topos

cohesive (∞,1)-topos

Models
Constructions
structures in a cohesive (∞,1)-topos

Contents
Idea
The notion of an elementary (∞,1)-topos is the analog of the notion of elementary topos in (∞,1)-category theory .

This is in contrast to the notion of an (∞,1)-topos equivalent to an (∞,1)-category of (∞,1)-sheaves , the analog of a sheaf topos , which is more specific (see geometric homotopy type theory ).

While every (∞,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 $(\infty,1)$ -topos should be defined as the larger class which is exactly the 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

Revised on January 8, 2015 01:19:25
by

Urs Schreiber
(195.113.30.252)