Infinity-Topos

Idea

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

Definition

An $(\infty ,1)$-topos generalizes the notion of topos to $\infty$-categories. It is an accessible left exact reflective sub-infinity-category of an $\infty$-category of infinity presheaves, i.e. a localization

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

where these functors are adjoints.

Background

Grothendieck Topos:

Definition

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

Link to original