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

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

\tableofcontents

\section{Presentation} \section{The continuum-flat axiom}

We shall begin be by using defining a combination of the objective abstract type continuum theory line version of homotopy type theory, described inhomotopy type theory$\mathbb{A}$ along to with be the an cohesive arbitrary homotopy non-trivial type commutative theory ring: developed there by are Mike terms Shulman.$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}$.

\subsection{Judgments Axiom and contexts}$\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 consists with of axiom four judgments:type judgments$\mathbb{A} \flat$ is called$\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; 𝔸</ins></span>}\mathrm{type}$ A \mathbb{A} \; \mathrm{type} , -cohesive where homotopy we type judge theory.$A$ to be a type, cohesive typing judgments, where we judge $a$ to cohesively be an element of $A$, $a:A$, crisp typing judgments, where we judge $a$ to crisply be an element of $A$, $a::A$, and context judgments, where we judge $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$. Contexts are lists of typing judgments $a:A$, $b:B$, $c:C$, et cetera, and crisp typing judgments $a::A$, $b::B$, $c::C$ et cetera, and are formalized by the rules for the empty context and extending the context by a cohesive typing judgment and a crisp typing judgment