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

\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

\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:

Let $\mathcal{J}$ be any arbitrary judgment. Then we have the following rules:

The weakening rule:

The substitution rule:

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:

Introduction rule for identity types:

Elimination rule for identity types:

Computation rules for identity types:

\section{External links}

• the nLab’s article on cohesive homotopy type theory