Let be a category with families, with presheaves and of “semantic types” and “semantic terms”. Given a finite set of variables , we define the presheaf of environments for to be . We will define, by structural induction on any term , and any any finite set of variables, the following partial morphisms of presheaves.
.
.
such that the composite is the second projection.
In fact, the third of these is not actually inductive at all: it is simply a semantic counterpart of the bidirectional mode-switching judgment. We define to be the domain restriction of
to the equalizer of
and the restriction of the second projection to its domain.
The inductive clauses of the definitions of and will be given below. This is an induction over raw syntax, but the clauses should be defined to precisely mirror the bidirectional rules of our type theory, using recursive calls to the above three operations as counterparts of the three syntactic judgments , , and (and checks for semantic equality as a counterpart of the syntactic equality judgments). This correspondence will then enable the proof of totality to proceed straightforwardly.
Inductive Clauses
Variables
If is a variable , then:
is the empty partial function (this might change with Russell universes).
If , then is the empty partial function.
If , then is the (total) projection onto the factor.
Constants
TODO
-types
include Initiality Project - Partial Interpretation - Pi-types?
Contexts
Now that we have interpreted raw terms as semantic terms and semantic types, we can interpret raw contexts as well. Suppose is a raw context, and let be the finite (ordered) set of variables occuring in . We define a sub-presheaf by induction on the length of as follows.
For the empty context , we have , the terminal presheaf.
For an extended context , with variables where , we inductively have . We also have (as defined above inductively) . Let be the intersection of and the domain of , and let be defined by the following pullback, where the bottom arrow is the composite .
We equip it with the composite , which is a composite of two monomorphisms and hence itself a monomorphism. Thus is indeed a sub-presheaf of as intended.