nLab Initiality Project - Partial Interpretation

Initiality Project - Partial Interpretation

Initiality Project - Partial Interpretation

This page is part of the Initiality Project.

Overview

Let CC be a category with families, with presheaves TyTy and TmTm of “semantic types” and “semantic terms”. Given a finite set of variables VVarV \subseteq Var, we define the presheaf of environments for VV to be Tm VTm^V. We will define, by structural induction on any term TT, and any any finite set VV of variables, the following partial morphisms of presheaves.

  1. T type V:Tm VTy\⟦ T \⟧ ^V_{type} : Tm^V \rightharpoonup Ty.
  2. T V:Tm VTm\⟦ T \⟧ ^V_{\Rightarrow} : Tm^V \rightharpoonup Tm.
  3. T V:Tm V×TyTm\⟦ T \⟧ ^V_{\Leftarrow} : Tm^V \times Ty \rightharpoonup Tm such that the composite Tm V×TyTmTyTm^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\⟦ T \⟧ ^V_{\Leftarrow} to be the domain restriction of

Tm V×Typr 1Tm VT VTm Tm^V \times Ty \xrightarrow{pr_1} Tm^V \overset{\⟦ T \⟧ ^V_{\Rightarrow}}{\rightharpoonup} Tm

to the equalizer of

Tm V×Typr 1Tm VT VTmTy 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×TyTm^V \times Ty to its domain.

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

Inductive Clauses

Variables

If TT is a variable xx, then:

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

Constants

TODO

Π\Pi-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 Γ\Gamma is a raw context, and let VV be the finite (ordered) set of variables occuring in Γ\Gamma. We define a sub-presheaf ΓTm V\⟦ \Gamma \⟧ \subseteq Tm^V by induction on the length of Γ\Gamma as follows.

  • For the empty context ()(), we have ()=Tm 0=1\⟦ () \⟧ = Tm^0 = 1, the terminal presheaf.
  • For an extended context (Γ,x:A)(\Gamma, x:A), with variables V{x}V \cup \{x\} where xVx\notin V, we inductively have ΓTm V\⟦ \Gamma \⟧ \subseteq Tm^V. We also have (as defined above inductively) A type V:Tm VTy\⟦ A \⟧^V_{type} : Tm^V \rightharpoonup Ty. Let UU be the intersection of Γ\⟦ \Gamma \⟧ and the domain of A type V\⟦ A \⟧^V_{type}, and let Γ,x:A\⟦ \Gamma, x:A \⟧ be defined by the following pullback, where the bottom arrow is the composite UTm VA type VTyU \hookrightarrow Tm^V \overset{\⟦ A \⟧^V_{type}}{\rightharpoonup} Ty .
    Γ,x:A Tm U Ty \array { \⟦ \Gamma, x:A \⟧ & \to & Tm \\ \downarrow & & \downarrow \\ U & \to & Ty }

    We equip it with the composite Γ,x:AU×TmTm V×Tm\⟦ \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 Γ,x:A\⟦ \Gamma, x:A \⟧ is indeed a sub-presheaf of Tm V{x}Tm V×TmTm^{V\cup \{x\}} \cong Tm^V \times Tm as intended.

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