nLab
geometric homotopy type theory
Contents
Context
Type theory
natural deduction metalanguage , practical foundations

type formation rule
term introduction rule
term elimination rule
computation rule
type theory (dependent , intensional , observational type theory , homotopy type theory )

syntax object language

= + +

/ -/
,
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 levels

semantics

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