\tableofcontents \section{Presentation} We use [[objective type theory]] as the base type theory of cohesive types, and build the theory of crisp judgments on top of objective type theory. \subsection{Judgments and contexts} Cohesive homotopy type theory consists of the following judgments: * Type judgments, where we judge $A$ to be a type, $A \; \mathrm{type}$ * Cohesive term judgments, where we judge $a$ to cohesively be an element of $A$, $a:A$ * Crisp term judgments, where we judge $a$ to crisply be an element of $A$, $a::A$ * Context judgments, where we judge $\Xi \vert \Gamma$ to be a context, $\Xi \vert \Gamma \; \mathrm{ctx}$. Contexts are lists of crisp term judgments $a::A$, $b::B$, $c::C$, et cetera, followed by lists of cohesive variable 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 crisp or cohesive variable judgment $$\frac{}{() \vert () \; \mathrm{ctx}} \qquad \frac{\Xi \vert () \; \mathrm{ctx} \quad \Xi \vert () \vdash A \; \mathrm{type}}{(\Xi, a::A) \vert () \; \mathrm{ctx}} \qquad \frac{\Xi \vert \Gamma \; \mathrm{ctx} \quad \Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert (\Gamma, a:A) \; \mathrm{ctx}}$$ \subsection{Structural rules} Within any dependent type theory, the structural rules include the [[variable rule]], the [[weakening rule]], and the [[substitution rule]]. In cohesive homotopy type theory these rules are only for cohesive term judgments. The variable rule states that we may derive a cohesive term judgment if the cohesive term judgment is in the context already: $$\frac{\Xi \vert \Gamma, a:A, \Delta \; \mathrm{ctx}}{\Xi \vert \Gamma, a:A, \Delta \vdash a:A}$$ Let $\mathcal{J}$ be any arbitrary judgment. Then we have the following rules: The weakening rule: $$\frac{\Xi \vert \Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Xi \vert \Gamma, a:A, \Delta \vdash \mathcal{J}}$$ The substitution rule: $$\frac{\Xi \vert \Gamma \vdash a:A \quad \Gamma, b:A, \Delta \vdash \mathcal{J}}{\Xi \vert \Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}$$ The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations. \subsection{Identity types} Formation rule for identity types: $$\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert \Gamma, a:A, b:A \vdash a =_A b \; \mathrm{type}}$$ Introduction rule for identity types: $$\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert \Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}$$ Elimination rule for identity types: $$\frac{\Xi \vert \Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{type} \quad \Xi \vert \Gamma, a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Xi \vert \Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash J(t, a, b, p):C(a, b, p)}$$ Computation rules for identity types: $$\frac{\Xi \vert \Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{type} \quad \Xi \vert \Gamma, a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Xi \vert \Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash \beta_{=_A}(a) : J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}$$ \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)) \section{External links} * the nLab's article on [[nlab:cohesive homotopy type theory]]