Homotopy Type Theory cohesive homotopy type theory > history (Rev #16)

\tableofcontents

\section{The continuum-flat axiom}

We begin by defining the abstract continuum 𝔸\mathbb{A} to be an arbitrary commutative ring with characteristic 0: there are terms 0:𝔸0:\mathbb{A} and 1:𝔸1:\mathbb{A} and functions (βˆ’)+(βˆ’):(𝔸×𝔸)→𝔸(-)+(-):(\mathbb{A} \times \mathbb{A}) \to \mathbb{A}, βˆ’(βˆ’):𝔸→𝔸-(-):\mathbb{A} \to \mathbb{A}, and (βˆ’)β‹…(βˆ’):(𝔸×𝔸)→𝔸(-)\cdot(-):(\mathbb{A} \times \mathbb{A}) \to \mathbb{A}, such that (𝔸,0,+,βˆ’)(\mathbb{A}, 0, +, -) is an abelian group, (𝔸,1,β‹…)(\mathbb{A}, 1, \cdot) is a commutative monoid, and β‹…\cdot distributes over ++.

𝔸\mathbb{A} has characteristic 0 if the unique ring homomorphism ℀→𝔸\mathbb{Z} \to \mathbb{A} is an embedding of types.

Axiom 𝔸♭\mathbb{A} \flat then states that for every crisp type AA, AA is discrete if and only if the function const:Aβ†’(𝔸→A)\mathrm{const}:A \to (\mathbb{A} \to A) is an equivalence of types.

Cohesive homotopy type theory with axiom 𝔸♭\mathbb{A} \flat is called 𝔸\mathbb{A}-cohesive homotopy type theory.

\subsection{The shape of a type}

\subsection{Contractibility of the shape of the continuum}

\subsection{Compact connectedness of the continuum}

\section{The circle}

Let us define the square function on 𝔸\mathbb{A} as a function (βˆ’) 2:𝔸→𝔸(-)^2:\mathbb{A} \to \mathbb{A} with a dependent function

def((βˆ’) 2):∏ x:𝔸:x 2= 𝔸xβ‹…x\mathrm{def}((-)^2):\prod_{x:\mathbb{A}}:x^2 =_\mathbb{A} x \cdot x

One definition of the abstract circle π•Š 1\mathbb{S}^1 is the (homotopy) coequalizer of the function x↦x+1x \mapsto x + 1 and the identity function id 𝔸\mathrm{id}_\mathbb{A}

π•Š 1≔coeq 𝔸,𝔸(id 𝔸,x↦x+1)\mathbb{S}^1 \coloneqq \mathrm{coeq}_{\mathbb{A}, \mathbb{A}}(\mathrm{id}_\mathbb{A}, x \mapsto x + 1)

An equivalent definition of the abstract circle π•Š 1\mathbb{S}^1 is the dependent sum type

π•Š 1β‰”βˆ‘ x:π”Έβˆ‘ y:𝔸x 2+y 2=1\mathbb{S}^1 \coloneqq \sum_{x:\mathbb{A}} \sum_{y:\mathbb{A}} x^2 + y^2 = 1

\section{See also}

\section{References}

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

  • Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)

  • Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)

  • Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)

Revision on October 23, 2022 at 02:36:02 by Anonymous?. See the history of this page for a list of all contributions to it.