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).

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 April 16, 2014 22:38:03 by David Corfield (46.208.3.134)