This page is part of the Initiality Project.

Let $C$ be a category with families, with presheaves $Ty$ and $Tm$ of “semantic types” and “semantic terms”. Given a finite set of variables $V \subseteq Var$, we define the **presheaf of environments** for $V$ to be $Tm^V$. We will define, by structural induction on any term $T$, and any any finite set $V$ of variables, the following partial morphisms of presheaves.

- $\⟦ T \⟧ ^V_{type} : Tm^V \rightharpoonup Ty$.
- $\⟦ T \⟧ ^V_{\Rightarrow} : Tm^V \rightharpoonup Tm$.
- $\⟦ T \⟧ ^V_{\Leftarrow} : Tm^V \times Ty \rightharpoonup Tm$ such that the composite $Tm^V \times Ty \rightharpoonup Tm \to Ty$ 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 $\⟦ T \⟧ ^V_{\Leftarrow}$ to be the domain restriction of

$Tm^V \times Ty \xrightarrow{pr_1} Tm^V \overset{\⟦ T \⟧ ^V_{\Rightarrow}}{\rightharpoonup} Tm$

to the equalizer of

$Tm^V \times Ty \xrightarrow{pr_1} Tm^V \overset{\⟦ T \⟧ ^V_{\Rightarrow}}{\rightharpoonup} Tm \to Ty$

and the restriction of the second projection $Tm^V \times Ty$ to its domain.

The inductive clauses of the definitions of $\⟦ T \⟧ ^V_{type}$ and $\⟦ T \⟧ ^V_{\Rightarrow}$ 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 $\Gamma \vdash A\,type$, $\Gamma \vdash T\Rightarrow A$, and $\Gamma \vdash T\Leftarrow A$ (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.

If $T$ is a variable $x$, then:

- $\⟦ x \⟧ ^V_{type}$ is the empty partial function (this might change with Russell universes).
- If $x\notin V$, then $\⟦ x \⟧ ^V_{\Rightarrow}$ is the empty partial function.
- If $x\in V$, then $\⟦ x \⟧ ^V_{\Rightarrow} : Tm^V \rightharpoonup Tm$ is the (total) projection onto the $x^{th}$ factor.

TODO

include Initiality Project - Partial Interpretation - Pi-types?

Now that we have interpreted raw terms as semantic terms and semantic types, we can interpret raw contexts as well. Suppose $\Gamma$ is a raw context, and let $V$ be the finite (ordered) set of variables occuring in $\Gamma$. We define a sub-presheaf $\⟦ \Gamma \⟧ \subseteq Tm^V$ by induction on the length of $\Gamma$ as follows.

- For the empty context $()$, we have $\⟦ () \⟧ = Tm^0 = 1$, the terminal presheaf.
- For an extended context $(\Gamma, x:A)$, with variables $V \cup \{x\}$ where $x\notin V$, we inductively have $\⟦ \Gamma \⟧ \subseteq Tm^V$. We also have (as defined above inductively) $\⟦ A \⟧^V_{type} : Tm^V \rightharpoonup Ty$. Let $U$ be the intersection of $\⟦ \Gamma \⟧$ and the domain of $\⟦ A \⟧^V_{type}$, and let $\⟦ \Gamma, x:A \⟧$ be defined by the following pullback, where the bottom arrow is the composite $U \hookrightarrow Tm^V \overset{\⟦ A \⟧^V_{type}}{\rightharpoonup} Ty$.$\array { \⟦ \Gamma, x:A \⟧ & \to & Tm \\ \downarrow & & \downarrow \\ U & \to & Ty }$
We equip it with the composite $\⟦ \Gamma, x:A \⟧ \to U \times Tm \to Tm^V \times Tm$, which is a composite of two monomorphisms and hence itself a monomorphism. Thus $\⟦ \Gamma, x:A \⟧$ is indeed a sub-presheaf of $Tm^{V\cup \{x\}} \cong Tm^V \times Tm$ as intended.

category: Initiality Project

Last revised on November 2, 2018 at 22:26:29. See the history of this page for a list of all contributions to it.