Showing changes from revision #11 to #12:
Added | Removed | Changed
\tableofcontents
\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 , where we judge to be a type, cohesive typing judgments, where we judge to cohesively be an element of , , crisp typing judgments, where we judge to crisply be an element of , , and context judgments, where we judge to be a context, . Contexts are lists of typing judgments , , , et cetera, and crisp typing judgments , , 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}
\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)