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