# nLab geometric homotopy type theory

### Context

#### Type theory

,

• ,

• $\vdash$ ,

(, , , )

• ,

• / ()

• // ()

= + +

/-/
,
of / of
introduction rule for for hom-tensor adjunction
( of) ( of)
into into
( of) ( of)
, ,
higher
/-//
/
, () ,
(, ) /
(absence of) (absence of)

• ,

• ,

• , ,

• ,

#### Homotopy theory

, ,

flavors: , , , , , , , …

models: , , , …

Introductions

Definitions

• ,

• ,

• ,

Paths and cylinders

Homotopy groups

Basic facts

Theorems

• -theorem

• //
• ,

• ,

• ,

• /

## Constructions

structures in a

• /

• /

• / homotopy groups

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