\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 rules state that we may derive a cohesive or crisp term judgment if the term judgment is in the context already: $$\frac{\Xi, a::A, \Delta \vert () \; \mathrm{ctx}}{\Xi, a::A, \Delta \vert () \vdash a::A} \quad \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 rules: $$\frac{\Xi, \Delta \vert () \vdash \mathcal{J} \quad \Xi \vert () \vdash A \; \mathrm{type}}{\Xi, a::A, \Delta \vert () \vdash \mathcal{J}} \qquad \frac{\Xi \vert \Gamma, \Delta \vdash \mathcal{J} \quad \Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert \Gamma, a:A, \Delta \vdash \mathcal{J}}$$ The substitution rules: $$\frac{\Xi \vert () \vdash a::A \quad \Xi, b::A, \Delta \vert () \vdash \mathcal{J}}{\Xi, \Delta[a/b] \vert () \vdash \mathcal{J}[a/b]} \qquad \frac{\Xi \vert \Gamma \vdash a:A \quad \Xi \vert \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} \quad \Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma \vdash b:A}{\Xi \vert \Gamma \vdash a =_A b \; \mathrm{type}}$$ * Introduction rule for identity types: $$\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \mathrm{refl}_A(a) : a =_A a}$$ * Elimination rule for identity types: $$\frac{\Xi \vert \Gamma, x:A, y:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma, z:A \vdash t:C[z/a, z/b, \mathrm{refl}_A(z)/p] \quad \Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma \vdash b:A \quad \Xi \vert \Gamma \vdash q:a =_A b}{\Xi \vert \Gamma \vdash \mathrm{ind}_{=_A}^{x.y.p.C}(z.t, a, b, q):C[a, b, q/x, y, p]}$$ * Computation rules for identity types: $$\frac{\Xi \vert \Gamma, x:A, y:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma, z:A \vdash t:C[z/a, z/b, \mathrm{refl}_A(z)/p] \quad \Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \beta_{=_A}^{x.y.p.C}(a):\mathrm{ind}_{=_A}^{x.y.p.C}(z.t, a, a, \mathrm{refl}(a)) =_{C[a, a, \mathrm{refl}_A(a)/x, y, p]} t}$$ \section{Sharp modality} * Formation rule for sharp types: $$\frac{\Xi, \Gamma \vert () \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \sharp A \; \mathrm{type}}$$ * Introduction rule for sharp types: $$\frac{\Xi, \Gamma \vert () \vdash a:A}{\Xi \vert \Gamma \vdash a^\sharp:\sharp A}$$ * Elimination rule for sharp types: $$\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash a_\sharp:A}$$ * Computation rule for sharp types: $$\frac{\Xi \vert () \vdash a:A}{\Xi \vert \Gamma \vdash \beta_\sharp(a):(a^\sharp)_\sharp =_A a}$$ * Uniqueness rule for sharp types: $$\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash \eta_\sharp(a):(a_\sharp)^\sharp =_{\sharp A} a}$$ \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]]