Infinity-Topos

Idea

A higher analogue of a Grothendieck topos, closed under the constructions needed to interpret HoTT (Π, Σ, Id types, universes, etc.).

Background

Grothendieck Topos:

Definition

A Grothendieck topos is just a category of sheaves on some site.

Link to original

Duplicate Content 1

$(\infty ,1)$-topoi generalize the notion of topos to $\infty$-categories.

an $(\infty ,1)$-topos is a accessible left exact reflective sub-infinity-category of an infinity category of infinity preseaves, if the localization

$$\subseteq :H\to PS{h}_{\infty }(C)$$ $$\mathrm{lex}:PS{h}_{\infty }(C)\to H$$

are ajoints.