# nLab geometric homotopy type theory

### Context

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

(∞,1)-topos theory

## Constructions

structures in a cohesive (∞,1)-topos

# Contents

## Idea

As the type theory of sheaf toposes (under the relation between category theory and type theory) is geometric type theory, so the homotopy type theory of (∞,1)-sheaf (∞,1)-toposes maybe deserves to be called geometric homotopy type theory.

Traditionally the types in geometric homotopy type theory, hence the geometric homotopy types, are known as ∞-stacks and maybe better as (∞,1)-sheaves, notably as moduli ∞-stacks.

## Examples

Revised on December 9, 2013 12:38:48 by Urs Schreiber (89.204.138.139)