nLab
geometric homotopy type theory

Context

Type theory

,

  • ,

    • \vdash ,

(, , , )

  • ,

  • / ()

  • // ()

= + +

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

  • ,

  • ,

    • , ,

  • ,

Homotopy theory

, ,

flavors: , , , , , , , …

models: , , , …

see also

Introductions

Definitions

  • ,

  • ,

      • ,

Paths and cylinders

Homotopy groups

Basic facts

Theorems

  • -theorem

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

Background

Definitions

    • //
  • ,

    • ,

Characterization

Morphisms

Extra stuff, structure and property

  • ,

Models

    • /

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.