# nLab elementary (infinity,1)-topos

### Context

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

(∞,1)-category theory

## Models

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

(∞,1)-topos theory

## 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

See maybe also the comments at

Revised on January 8, 2015 01:19:25 by Urs Schreiber (195.113.30.252)