\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 $$\mathrm{def}(s):\prod_{x:\mathbb{A}}:s(x) =_\mathbb{A} x + 1$$ and the square function on $\mathbb{A}$ as a function $(-)^2:\mathbb{A} \to \mathbb{A}$ with a dependent function $$\mathrm{def}((-)^2):\prod_{x:\mathbb{A}}:x^2 =_\mathbb{A} x \cdot x$$ 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 $$\sum_{x:\mathbb{A}} \sum_{y:\mathbb{A}} x^2 + y^2 = 1$$ \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](https://arxiv.org/abs/1509.07584), [doi:10.1017/S0960129517000147](https://doi.org/10.1017/S0960129517000147)) * *Homotopy Type Theory: Univalent Foundations of Mathematics*, The Univalent Foundations Program, Institute for Advanced Study, 2013. ([web](http://homotopytypetheory.org/book/), [pdf](http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf)) * Egbert Rijke, *Introduction to Homotopy Type Theory*, Cambridge Studies in Advanced Mathematics, Cambridge University Press ([pdf](https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.pdf)) (478 pages) * Benno van den Berg, Martijn den Besten, *Quadratic type checking for objective type theory* ([arXiv:2102.00905](https://arxiv.org/abs/2102.00905))