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 with variables .
- If is derivable, then the domain of contains .
- If is derivable, then the domain of contains , and the composite agrees with on .
- If is derivable, then the domain of contains the subobject defined by .
- If is derivable, then and agree when their domains are intersected with each other and also with .
- If is derivable, then and agree when their domains are intersected with each other and also with the subobject 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
-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:
Proof
By induction on the length of . If it is empty, then , the terminal presheaf, which is representable as our CwF has a terminal object.
For a context extension , by induction we have representable. Recall that is defined as a pullback
Since is, by our definition of CwF, a representable morphism, it will therefore suffice to show that is a representable object.
Now is by definition the intersection of with the domain of . But since is valid, is derivable, so by the local totality theorem, the domain of contains . Thus, , which is representable by the inductive hypothesis.
Furthermore, since is algebraically represented, at each step we obtain a specified representing object for . We henceforth abusively denote this object of also by .
Combining this with the local totality theorem, we can extract more traditional-looking interpretations of derivable judgments with valid contexts that are “purely inside ” rather than phrased in terms of presheaves.
- If is valid and is derivable, we have (by local totality) a total morphism , hence (by the Yoneda lemma) an element of the set , which we may denote .
- If is valid and is derivable, we have a total morphism , hence an element of the set which we may denote . By the rest of the local totality theorem for type synthesis, the underlying semantic type of this semantic term is .
- If is valid and is derivable, we similarly obtain an element of , whose underlying semantic type is .