nLab
geometric homotopy type theory

Contents

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

(,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

As geometric type theory refers to a conjectural extension of geometric logic to an extensional dependent type theory that corresponds to sheaf toposes (under the relation between category theory and type theory) with geometric morphisms between them, a similar conjectural extension to a homotopy type theory corresponding to (∞,1)-sheaf (∞,1)-toposes (and geometric morphisms) 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

Last revised on April 17, 2018 at 11:27:51. See the history of this page for a list of all contributions to it.