\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:\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}$ 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 $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. \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:\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 the function $x \mapsto x + 1$ and the identity function $\mathrm{id}_\mathbb{A}$ $$\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 $\mathbb{S}^1$ is the dependent sum type $$\mathbb{S}^1 \coloneqq \sum_{x:\mathbb{A}} \sum_{y:\mathbb{A}} x^2 + y^2 = 1$$ \section{See also} * [[homotopy type theory]] * [[high school mathematics in cohesive 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))