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

\tableofcontents

\section{The continuum-flat axiom}

We begin by defining the abstract continuum line $\mathbb{A}$ to be an arbitrary non-trivial commutative ring: there are terms $0:\mathbb{A}$ and $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 $(\mathbb{A}, 0, +, -)$ is an abelian group, $(\mathbb{A}, 1, \cdot)$ is a commutative monoid, and $\cdot$ distributes over $+$. $\mathbb{A}$ is non-trivial if there is a witness $p:(0 =_\mathbb{A} 1) \to \mathbb{0}$.

Axiom $\mathbb{A} \flat$ then states that for every crisp type $A$, $A$ is discrete if and only if the function $\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.

Let us define the successor function on $\mathbb{A}$ as a function $s:\mathbb{A} \to \mathbb{A}$ with a dependent function

and the square function on $\mathbb{A}$ as a function $(-)^2:\mathbb{A} \to \mathbb{A}$ with a dependent function

One definition of the abstract circle $\mathbb{S}^1$ is the (homotopy) coequalizer of $s$ and the identity function $\mathrm{id}_\mathbb{A}$. An equivalent definition of the abstract circle $\mathbb{S}^1$ is the dependent sum type

\section{See also}

• homotopy type theory

\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)