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

Showing changes from revision #19 to #20: Added | Removed | Changed

\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}$