nLab
geometric homotopy type theory
Context
Type theory
Homotopy theory
homotopy theory , (∞,1)-category theory , homotopy type theory

flavors: stable , equivariant , rational , p-adic , proper , geometric , cohesive , directed …

models: topological , simplicial , localic , …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

$(\infty,1)$ -Topos Theory
(∞,1)-topos theory

Background
Definitions
elementary (∞,1)-topos

(∞,1)-site

reflective sub-(∞,1)-category

(∞,1)-category of (∞,1)-sheaves

(∞,1)-topos

(n,1)-topos , n-topos

(∞,1)-quasitopos

(∞,2)-topos

(∞,n)-topos

Characterization
Morphisms
Extra stuff, structure and property
hypercomplete (∞,1)-topos

over-(∞,1)-topos

n-localic (∞,1)-topos

locally n-connected (n,1)-topos

structured (∞,1)-topos

locally ∞-connected (∞,1)-topos , ∞-connected (∞,1)-topos

local (∞,1)-topos

cohesive (∞,1)-topos

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