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

\section{Presentation}

We shall be using a combination of the objective type theory version of homotopy type theory, described in homotopy type theory along with the cohesive homotopy type theory developed by Mike Shulman.

\subsection{Judgments and contexts}

Cohesive homotopy type theory consists of four judgments: type judgments $A \; \mathrm{type}$, where we judge $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

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