Internal Parametricity without an Interval

Proof. Items 1–3 and the isomorphism of item 4 are the corresponding equations of definition 167.3, definition 167.4; only the claim about projections needs an argument, and it is a calculation:  ◻

Proof. For 1, $a=a[\star /\mathrm{\_}]$, so ${\mathsf{R}}_{A}a={\mathsf{R}}_A(a[\star /\mathrm{\_}])=\mathsf{ap}(\mathrm{\_}.a)({\mathsf{R}}_{\mathbf{1}}\star )$ by the second Legs equation, and ${\mathsf{R}}_{\mathbf{1}}\star =\star$ because $\mathrm{\forall }\mathbf{1}=\mathbf{1}$ is a unit type.

For 2, both sides equal $\mathsf{ap}(\mathrm{\_}.b)\star$: $$\mathsf{ap}(\mathrm{\_}.b)a_2\stackrel{b=b[\star /\mathrm{\_}]}{=}\mathsf{ap}(\mathrm{\_}.b)(\mathsf{ap}(\mathrm{\_}.\star )a_2)\stackrel{\mathrm{\forall }\mathbf{1}=\mathbf{1}}{=}\mathsf{ap}(\mathrm{\_}.b)\star ,$$ the second step because $\mathsf{ap}(\mathrm{\_}.\star )a_2$ is an element of $\mathrm{\forall }\mathbf{1}=\mathbf{1}$ and so is $\star$.

For 3, apply the $\mathrm{\Sigma }$-uniqueness rule to $k_{\sum _{x:A}B}(a_2,b_2)$ and compute the first projection by the first Legs equation applied to $\mathsf{ap}(w.{\mathsf{pr}}_{1}w)$, using the $\mathrm{\Sigma }$ equation of definition 167.3; the second projection is $k^{\mathsf{d}}$ by its definition in definition 167.2.

For 4, apply 3 to $(a_2,\mathsf{apd}(x.t)a_2)=\mathsf{apd}(x.(x,t))a_2$ and use the first Legs equation on the right-hand side. ◻

Proof. By induction on $I_0$. At $I_0=0$ both are identities by definition. At $1+I_0$, using functoriality of $\mathsf{suc}$ at the middle step. The other composite is the same calculation with the two definitions exchanged. ◻

Proof. Proof structure. The core theory is interpreted by the standard presheaf model of chapter 52: contexts are presheaves, types over $\mathrm{\Gamma }$ are presheaves on the category of elements, and the formers of definition 167.1 are the pointwise ones, with $\mathcal{U}$ a Hofmann–Streicher universe. What must be added is the interpretation of the span structure, and each item of definition 167.8 is one line.

The endofunctor. Set $(\mathrm{\forall }\mathrm{\Gamma }{)}_I:={\mathrm{\Gamma }}_{1+I}$, with the action of $f:◻(J,I)$ given by $\mathsf{suc}f$. Functoriality is the first two equations of definition 167.10, and preservation of the terminal presheaf is immediate since $\mathbf{1}$ is the constant one-point presheaf. The action on types and terms is the same reindexing, so it commutes with substitution.

The three transformations. Set $k_{\mathrm{\Gamma }}$, ${\mathsf{R}}_{\mathrm{\Gamma }}$ and ${\mathsf{S}}_{\mathrm{\Gamma }}$ to be precomposition by $k_I$, ${\mathsf{R}}_I$ and ${\mathsf{S}}_I$. Naturality is the third, fourth and fifth equations of definition 167.10, contravariantly; the remaining four equations of definition 167.10 become, again contravariantly, the four equations required in definition 167.8, with the braid equation last.

Strict preservation. $\mathbf{1}$, $\mathrm{\Sigma }$, ${\mathsf{Eq}}_{}(,)$ and $\mathbf{2}$ are interpreted pointwise, and reindexing along $\mathsf{suc}$ commutes with a pointwise former; hence each is preserved on the nose.

$\mathrm{\Pi }$ and $\mathcal{U}$. Neither is pointwise. For $\mathrm{\Pi }$, an element of $\mathrm{\forall }(\mathrm{\Pi }BC)$ at $I$ is an element of $(\mathrm{\Pi }BC)$ at $1+I$, which is a family of functions indexed by morphisms out of $1+I$; splitting those morphisms according to whether they factor through $k$ gives exactly the triple $(t_k,t,e)$ of MkPi, and the splitting is a bijection by the case analysis on $◻$-morphisms that lemma 167.11 makes available. For $\mathcal{U}$, the canonical map to the span of its decodings has a section by the same case analysis; the reverse round trip is not the identity in this model, which is why definition 167.4 asks only for a section and definition 167.3 lists only the three Universe equations. ◻

Proof. For $\mathrm{\forall }$, unfolding the two definitions at dimension $I$, For $k$, $$G{k}_{\mathrm{\Gamma }}{\gamma }^{1+I}\stackrel{def.ofG}{=}{\mathrm{\forall }}^I{k}_{\mathrm{\Gamma }}\circ {\gamma }^{1+I}\stackrel{definition167.10}{=}{\gamma }^{1+I}[k_I]\stackrel{def.}{=}{k}_{G\mathrm{\Gamma }}{\gamma }^{1+I},$$ and the arguments for $\mathsf{R}$ and $\mathsf{S}$ are the same computation with ${\mathsf{R}}_I$ and ${\mathsf{S}}_I$ in place of $k_I$, using the corresponding generator of definition 167.10. ◻

Proof. Global syntax. Glue along $G$, using lemma 167.14 to know that the displayed model of definition 167.13 is a model of the global theory. Induction on $\mathrm{Syn}$ interprets a closed $t:\mathbf{2}$ as a term of $${\mathrm{Tm}}_{[{◻}^{\mathrm{op}},\mathbf{Set}]}(G\cdot \mathbf{1}.)(\sum _{:\mathbf{2}}{\mathsf{Eq}}_{}(\mathsf{ite}\mathbf{q}(G\mathsf{tt}[\mathbf{p}])(G\mathsf{ff}[\mathbf{p}]),Gt[\mathbf{p}])).$$ Supplying ${\mathrm{id}}_{\cdot }$ and the element of the metatheoretic unit set yields a pair consisting of a metatheoretic Boolean $b$ together with a proof that $\mathsf{ite}b\mathsf{tt}\mathsf{ff}=t$; case analysis on $b$ gives the two alternatives.

Local syntax. Let $t$ be closed of type $\mathbf{2}$ in the local syntax. By theorem 167.9, $\alpha t$ is a closed term of type $\mathbf{2}$ in the global syntax, since $\alpha$ acts as the identity on the core theory and $\mathbf{2}$, $\cdot$ belong to it. The previous paragraph gives, say, $\alpha t=\mathsf{tt}$. Applying $\beta$ and using that $\beta$ also fixes the core theory, $$t\stackrel{\beta \alpha =\mathrm{id}}{=}\beta (\alpha t)\stackrel{hypothesis}{=}\beta \mathsf{tt}\stackrel{\beta fixesthecore}{=}\mathsf{tt}.$$ ◻

Proof. The unary calculus suffices, so $k$ has one value.

The span. Let $x:A⊢P$ be any predicate and let $p:P[a/x]$. Form $$s:=\mathsf{unspan}A(\sum _{x:A}P)(x.{\mathsf{pr}}_{1}x):\mathrm{\forall }\mathcal{U},$$ whose leg is $A$, whose apex is $\sum _{x:A}P$, and whose projection is the first projection. Then $(s,(a,p))$ is an element of $\mathrm{\forall }(\sum _{y:\mathcal{U}}\mathsf{El}(y))$, by the $\mathrm{\Sigma }$ equation of definition 167.3 together with the second Universe equation.

The term. Apply $\mathsf{apd}$ to $f$: $$u:=\mathsf{apd}(x.fx)(s,(a,p)).$$ Its type computes as

The first component. Compute ${\mathsf{pr}}_{1}u$: using in the last step that the leg of $s$ is $A$, whose code is $c_A$, and that the projection sends $(a,p)$ to $a$.

Conclusion. Hence ${\mathsf{pr}}_{2}u:P[f(c_A,a)/x]$. Choose $P:={\mathsf{Eq}}_A(a,x)$ and $p:=\mathsf{refl}$; then ${\mathsf{pr}}_{2}u:{\mathsf{Eq}}_A(a,f(c_A,a))$, and symmetry of the extensional identity type gives the stated inhabitant. ◻