nLab
elementary (infinity,1)-topos

Context

(,1)(\infty,1)-Category theory

(,1)(\infty,1)-Topos Theory

(∞,1)-topos theory

Background

Definitions

Characterization

Morphisms

Extra stuff, structure and property

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 (,1)(\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

Revised on October 1, 2014 14:32:11 by Bas Spitters (85.17.92.143)