nLab cohesive homotopy type theory with two kinds of types

Contents

under construction

Contents

Introduction

In Shulman18, the authors write

One might argue that it would be better to include a separate kind of type representing objects in the base category, and type constructors represent-ing the functors p *p_*, p *p^*, etc. rather than the monads and comonads they induce. This would be in line with the “judgmental deconstruction” of Reed (2009) that decomposes \Box and \bigcirc into pairs of adjoint functors. It could be that this is indeed better; in fact, the current rules for \flat and \sharp were deduced from a generalization of Reed (2009) developed by Licata and Shulman (2016).

This is an attempt at developing such a cohesive homotopy type theory.

Overview

This presentation of cohesive homotopy type theory is a dependent type theory consisting of two different kinds of types, spaces and homotopy types. 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 product type.

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

ʃ(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)

Sources

Created on June 19, 2022 at 19:30:27. See the history of this page for a list of all contributions to it.