real-cohesive homotopy type theory in nLab

Contents

Idea

ℝ\mathbb{R}-cohesive homotopy type theory or real-cohesive homotopy type theory is a version of cohesive homotopy type theory which has the axiom of real cohesion. It provides a synthetic foundation for topology, real analysis, classical homotopy theory, and algebraic topology. A model of real-cohesive homotopy type theory is the Euclidean-topological infinity-groupoids.

Presentation

We assume a spatial type theory presented with crisp term judgments a::Aa::A. In addition, we also assume the spatial type theory has a Dedekind real numbers type ℝ\mathbb{R}, and ℝ\mathbb{R}-localizations ℒ ℝ(−)\mathcal{L}_{\mathbb{R}}(-).

Given a type AA, let us define const A,ℝ:A→(ℝ→A)\mathrm{const}_{A, \mathbb{R}}:A \to (\mathbb{R} \to A) to be the type of all constant functions in the Dedekind real numbers ℝ\mathbb{R}:

δ const A,ℝ(a,r):const A,ℝ(a)(r)= Aa\delta_{\mathrm{const}_{A, \mathbb{R}}}(a, r):\mathrm{const}_{A, \mathbb{R}}(a)(r) =_A a

There is an equivalence const A,1:A≃(1→A)\mathrm{const}_{A, 1}:A \simeq (1 \to A) between the type AA and the type of functions from the unit type 11 to AA. Given types BB and CC and a function F:(B→A)→(C→A)F:(B \to A) \to (C \to A), type AA is FF-local if the function F:(B→A)→(C→A)F:(B \to A) \to (C \to A) is an equivalence of types.

A crisp type Ξ|()⊢A\Xi \vert () \vdash A is discrete if the function (−) ♭:♭A→A(-)_\flat:\flat A \to A is an equivalence of types.

The axiom of ℝ\mathbb{R}-cohesion states that for the crisp affine line Ξ|()⊢ℝtype\Xi \vert () \vdash \mathbb{R} \; \mathrm{type}, given any crisp type Ξ|()⊢Atype\Xi \vert () \vdash A \; \mathrm{type}, AA is discrete if and only if AA is (const A,1 −1∘const A,ℝ)(\mathrm{const}_{A, 1}^{-1} \circ \mathrm{const}_{A, \mathbb{R}})-local.

This allows us to define discreteness for non-crisp types: a type AA is discrete if AA is (const A,1 −1∘const A,ℝ)(\mathrm{const}_{A, 1}^{-1} \circ \mathrm{const}_{A, \mathbb{R}})-local.

The shape modality in ℝ\mathbb{R}-cohesive homotopy type theory is then defined as the ℝ\mathbb{R}-localization ʃ(A)≔ℒ ℝ(A)\esh(A) \coloneqq \mathcal{L}_{\mathbb{R}}(A), which ensures that the shape of ℝ\mathbb{R} itself is a contractible type.

 See also

• cohesive homotopy type theory
• axiom of real cohesion
• Euclidean-topological infinity-groupoid

References

• Mike Shulman: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science 28 6 (2018) 856-941 [arXiv:1509.07584, doi:10.1017/S0960129517000147]