\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** $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 $$\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{type}}{(\Gamma, a:A) \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{type}}{(\Gamma, a::A) \; \mathrm{ctx}}$$ \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](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))