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 to be a type,
Cohesive term judgments, where we judge to cohesively be an element of ,
Crisp term judgments, where we judge to crisply be an element of ,
Context judgments, where we judge to be a context, .
Contexts are lists of crisp term judgments , , , et cetera, followed by lists of cohesive variable judgments , , , 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 rules state that we may derive a cohesive or crisp term judgment if the term judgment is in the context already:
Let be any arbitrary judgment. Then we have the following rules:
The weakening rules:
The substitution rules:
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.