nLab Initiality Project - Totality

Initiality Project - Totality

This page is part of the Initiality Project.

Overview

We now prove that the partial interpretations of types, terms, and contexts satisfy the following “local” totality properties, for any raw context $\Gamma$ with variables $V$.

1. If $\Gamma \vdash A\, type$ is derivable, then the domain of $\⟦ A \⟧^V_{type} : Tm^V \rightharpoonup Ty$ contains $\⟦\Gamma\⟧$.
2. If $\Gamma \vdash T \Rightarrow A$ is derivable, then the domain of $\⟦ T \⟧^V_{\Rightarrow} : Tm^V \rightharpoonup Tm$ contains $\⟦\Gamma\⟧$, and the composite $Tm^V \overset{\⟦ T \⟧^V_{\Rightarrow}}{\rightharpoonup} Tm \to Ty$ agrees with $\⟦ A \⟧^V_{type}$ on $\⟦\Gamma\⟧$.
3. If $\Gamma \vdash T \Leftarrow A$ is derivable, then the domain of $\⟦ T \⟧^V_{\Leftarrow} : Tm^V \times Ty \rightharpoonup Tm$ contains the subobject defined by $\⟦\Gamma\⟧ \hookrightarrow Tm^V \overset{(id,\⟦ A \⟧^V_{type})}{\rightharpoonup} Tm^V \times Ty$.
4. If $\Gamma \vdash A \equiv B \, type$ is derivable, then $\⟦ A \⟧^V_{type}$ and $\⟦ B \⟧^V_{type}$ agree when their domains are intersected with each other and also with $\⟦\Gamma\⟧$.
5. If $\Gamma \vdash S \equiv T : A$ is derivable, then $\⟦ S \⟧^V_{\Leftarrow}$ and $\⟦ T \⟧^V_{\Leftarrow}$ agree when their domains are intersected with each other and also with the subobject $\⟦\Gamma\⟧ \hookrightarrow Tm^V \times Ty$ defined in (3) above.

The proof is by mutual induction on these mutually defined inductive judgments; thus we have one clause for each primitive rule in our type theory.

Inductive clauses

Variables

Mode-switching

Equality

Constants

$\Pi$-types

include Initiality Project - Totality - Pi-types?

Valid Contexts

The above totality theorem is called “local” because it only says the interpretations are defined on the interpretation of the context; if the context is invalid then the latter interpretation could be empty. However, with the local totality theorem in hand, we can deduce a global totality theorem for valid contexts. Note that this parallels how the notion of valid context was defined after giving the inductive definition of the judgments, and also how the partial interpretation of contexts was defined after giving the partial interpretations of types and terms.

The global totality theorem is:

Theorem

If $\Gamma$ is a valid context, then $\⟦ \Gamma \⟧$ is a representable presheaf.

Proof

By induction on the length of $\Gamma$. If it is empty, then $\⟦ () \⟧ = 1$, the terminal presheaf, which is representable as our CwF $C$ has a terminal object.

For a context extension $(\Gamma,x:A)$, by induction we have $\⟦ \Gamma \⟧$ representable. Recall that $\⟦\Gamma,x:A\⟧$ is defined as a pullback

$$\array { \⟦ \Gamma, x:A \⟧ & \to & Tm \\ \downarrow & & \downarrow \\ U & \to & Ty. }$$

Since $Tm\to Ty$ is, by our definition of CwF, a representable morphism, it will therefore suffice to show that $U$ is a representable object.

Now $U$ is by definition the intersection of $\⟦\Gamma\⟧$ with the domain of $\⟦ A \⟧^V_{type}$. But since $(\Gamma,x:A)$ is valid, $\Gamma \vdash A \, type$ is derivable, so by the local totality theorem, the domain of $\⟦ A \⟧^V_{type}$ contains $\⟦ \Gamma \⟧$. Thus, $U = \⟦ \Gamma \⟧$, which is representable by the inductive hypothesis.

Furthermore, since $Tm\to Ty$ is algebraically represented, at each step we obtain a specified representing object for $\⟦\Gamma\⟧$. We henceforth abusively denote this object of $C$ also by $\⟦\Gamma\⟧$.

Combining this with the local totality theorem, we can extract more traditional-looking interpretations of derivable judgments with valid contexts that are “purely inside $C$” rather than phrased in terms of presheaves.

• If $\Gamma$ is valid and $\Gamma \vdash A\,type$ is derivable, we have (by local totality) a total morphism $\⟦ \Gamma \⟧ \xrightarrow{\⟦ A \⟧^V_{type}} Ty$, hence (by the Yoneda lemma) an element of the set $Ty(\⟦ \Gamma\⟧)$, which we may denote $\⟦ A \⟧^\Gamma_{type}$.
• If $\Gamma$ is valid and $\Gamma \vdash T \Rightarrow A$ is derivable, we have a total morphism $\⟦ \Gamma \⟧ \xrightarrow{\⟦ A \⟧^V_{\Rightarrow}} Tm$, hence an element of the set $Tm(\⟦ \Gamma\⟧)$ which we may denote $\⟦ T \⟧^\Gamma_{\Rightarrow}$. By the rest of the local totality theorem for type synthesis, the underlying semantic type of this semantic term is $\⟦ A \⟧^\Gamma_{type}$.
• If $\Gamma$ is valid and $\Gamma \vdash T \Leftarrow A$ is derivable, we similarly obtain an element $\⟦ T \⟧^\Gamma_{\Leftarrow A}$ of $Tm(\⟦ \Gamma\⟧)$, whose underlying semantic type is $\⟦ A \⟧^\Gamma_{type}$.

category: Initiality Project