Homotopy Type Theory cohesive homotopy type theory > history (Rev #14, changes)

Showing changes from revision #13 to #14: Added | Removed | Changed

\tableofcontents

\section{The continuum-flat axiom}

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

Axiom $\mathbb{A}$$\mathbb{A} \flat$ has characteristic 0 if the unique ring homomorphism then states that for every crisp type $\mathbb{Z} \to \mathbb{A}$$A$ is an embedding of types., $A$ is discrete if and only if the function $\mathrm{const}:A \to (\mathbb{A} \to A)$ is an equivalence of types.

Cohesive Axiom homotopy type theory with axiom$\mathbb{A} \flat$ is then called states that for every crisp type$\mathrm{<span><del\; class="diffmod">\; 𝔸</del><ins\; class="diffmod">\; A</ins></span>}$ \mathbb{A} A -cohesive , homotopy type theory.$A$ is discrete if and only if the function $\mathrm{const}:A \to (\mathbb{A} \to A)$ is an equivalence of types.

Let Cohesive us homotopy define type the theory successor with function axiom on$𝔸♭$ \mathbb{A} \flat as is a called function$s:𝔸\to 𝔸$ s:\mathbb{A} \to \mathbb{A} -cohesive with homotopy a type dependent theory. function