nLab Initiality Project - Totality

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 VV.

  1. If ΓAtype\Gamma \vdash A\, type is derivable, then the domain of A type V:Tm VTy\⟦ A \⟧^V_{type} : Tm^V \rightharpoonup Ty contains Γ\⟦\Gamma\⟧.
  2. If ΓTA\Gamma \vdash T \Rightarrow A is derivable, then the domain of T V:Tm VTm\⟦ T \⟧^V_{\Rightarrow} : Tm^V \rightharpoonup Tm contains Γ\⟦\Gamma\⟧, and the composite Tm VT VTmTyTm^V \overset{\⟦ T \⟧^V_{\Rightarrow}}{\rightharpoonup} Tm \to Ty agrees with A type V\⟦ A \⟧^V_{type} on Γ\⟦\Gamma\⟧.
  3. If ΓTA\Gamma \vdash T \Leftarrow A is derivable, then the domain of T V:Tm V×TyTm\⟦ T \⟧^V_{\Leftarrow} : Tm^V \times Ty \rightharpoonup Tm contains the subobject defined by ΓTm V(id,A type V)Tm V×Ty\⟦\Gamma\⟧ \hookrightarrow Tm^V \overset{(id,\⟦ A \⟧^V_{type})}{\rightharpoonup} Tm^V \times Ty.
  4. If ΓABtype\Gamma \vdash A \equiv B \, type is derivable, then A type V\⟦ A \⟧^V_{type} and B type V\⟦ B \⟧^V_{type} agree when their domains are intersected with each other and also with Γ\⟦\Gamma\⟧.
  5. If ΓST:A\Gamma \vdash S \equiv T : A is derivable, then S V\⟦ S \⟧^V_{\Leftarrow} and T V\⟦ T \⟧^V_{\Leftarrow} agree when their domains are intersected with each other and also with the subobject ΓTm V×Ty\⟦\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\⟦ () \⟧ = 1, the terminal presheaf, which is representable as our CwF CC has a terminal object.

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

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

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

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

Furthermore, since TmTyTm\to Ty is algebraically represented, at each step we obtain a specified representing object for Γ\⟦\Gamma\⟧. We henceforth abusively denote this object of CC 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 CC” rather than phrased in terms of presheaves.

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

Last revised on October 30, 2018 at 22:01:13. See the history of this page for a list of all contributions to it.