Homotopy Type Theory cohesive homotopy type theory > history (changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

Contents

Overview

Cohesive homotopy type theory is a two-sorted dependent type theory of spaces and homotopy types, where there exist judgments

  • for spaces

    ΓΓSspace\frac{\Gamma}{\Gamma \vdash S\ space}
  • for homotopy types

    ΓΓThomotopytype\frac{\Gamma}{\Gamma \vdash T\ homotopy\ type}
  • for points

    ΓSspaceΓs:S\frac{\Gamma \vdash S\ space}{\Gamma \vdash s:S}
  • for terms

    ΓThomotopytypeΓt:T\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash t:T}
  • for fibrations

    ΓSspaceΓ,s:SA(s)space\frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash A(s)\ space}
  • for dependent types

    ΓThomotopytypeΓ,t:TB(t)homotopytype\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash B(t)\ homotopy\ type}
  • for sections

    ΓSspaceΓ,s:Sa(s):A(s)\frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash a(s):A(s)}
  • for dependent terms

    ΓThomotopytypeΓ,t:Tb(t):B(t)\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash b(t):B(t)}

Cohesive homotopy type theory has the following additional judgments, 2 for turning spaces into homotopy types and the other two for turning homotopy types into spaces:

  • Every space has an underlying homotopy type

    ΓSspaceΓp *(S)homotopytype\frac{\Gamma \vdash S\ space}{\Gamma \vdash p_*(S)\ homotopy\ type}
  • Every space has a fundamental homotopy type

    ΓSspaceΓp !(S)homotopytype\frac{\Gamma \vdash S\ space}{\Gamma \vdash p_!(S)\ homotopy\ type}
  • Every homotopy type has a discrete space

    ΓThomotopytypeΓp *(T)space\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^*(T)\ space}
  • Every homotopy type has an indiscrete space

    ΓThomotopytypeΓp !(T)space\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^!(T)\ space}

The underlying homotopy type and fundamental homotopy type are sometimes represented by the greek letters Γ\Gamma and Π\Pi respectively, but both are already used in dependent type theory to represent the context and the dependent/indexed product.

Modalities

From these judgements one could construct the sharp? modality? as

(S)p !(p *(S))\sharp(S) \coloneqq p^!(p_*(S))

the flat? modality as

(S)p *(p *(S))\flat(S) \coloneqq p^*(p_*(S))

and the shape modality as

esh(S)p *(p !(S))\esh(S) \coloneqq p^*(p_!(S))

for a space SS.

Other types

Path spaces

Γ,a:S,b:SΓa= Sbspace\frac{\Gamma, a:S, b:S}{\Gamma \vdash a =_S b\ space}

Identity types

Γ,a:T,b:TΓa= Tbhomotopytype\frac{\Gamma, a:T, b:T}{\Gamma \vdash a =_T b\ homotopy\ type}

Mapping spaces

Γ,Aspace,BspaceΓABspace\frac{\Gamma, A\ space, B\ space}{\Gamma \vdash A \to B\ space}

Function types

Γ,Ahomotopytype,BhomotopytypeΓABhomotopytype\frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma \vdash A \to B\ homotopy\ type}

Section spaces

Γ,s:SA(s)spaceΓ s:SA(s)space\frac{\Gamma, s:S \vdash A(s)\ space}{\Gamma \vdash \prod_{s:S} A(s)\ space}

Dependent function types

Γ,t:TA(t)homotopytypeΓ t:TA(t)homotopytype\frac{\Gamma, t:T \vdash A(t)\ homotopy\ type}{\Gamma \vdash \prod_{t:T} A(t)\ homotopy\ type}

Product spaces

Γ,Aspace,BspaceΓA×Bspace\frac{\Gamma, A\ space, B\ space}{\Gamma \vdash A \times B\ space}

Pair types

Γ,Ahomotopytype,BhomotopytypeΓA×Bhomotopytype\frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma \vdash A \times B\ homotopy\ type}

Total spaces

Γ,s:SA(s)spaceΓ s:SA(s)space\frac{\Gamma, s:S \vdash A(s)\ space}{\Gamma \vdash \sum_{s:S} A(s)\ space}

Dependent pair types

Γ,t:TA(t)homotopytypeΓ t:TA(t)homotopytype\frac{\Gamma, t:T \vdash A(t)\ homotopy\ type}{\Gamma \vdash \sum_{t:T} A(t)\ homotopy\ type}

Unit space

ΓΓ𝟙space\frac{\Gamma}{\Gamma \vdash \mathbb{1}\ space}

Unit type

ΓΓ𝟙homotopytype\frac{\Gamma}{\Gamma \vdash \mathbb{1}\ homotopy\ type}

Other properties

The fundamental homotopy type of the unit space is equivalent to the unit type.

p !(𝟙)𝟙p_!(\mathbb{1}) \cong \mathbb{1}

The product of the fundamental homotopy types of spaces AA and BB is equivalent to the fundamental homotopy type of the product of spaces AA and BB:

p !(A×B)p !(A)×p !(B)p_!(A \times B) \cong p_!(A) \times p_!(B)

Last revised on June 19, 2022 at 19:43:34. See the history of this page for a list of all contributions to it.