ch:rules-of-dtt: ch:rules-of-dtt

The direct presuppositions are $$\mathrm{\Gamma },x:A⊢a:B\text{and}\mathrm{\Gamma },x:A⊢b:B.$$ Each term judgment presupposes $\mathrm{\Gamma },x:A⊢B\mathsf{type}$, which in turn presupposes $\mathrm{\Gamma },x:A\mathsf{ctx}$. Context formation then gives $\mathrm{\Gamma }⊢A\mathsf{type}$ and $\mathrm{\Gamma }\mathsf{ctx}$. If $\mathrm{\Gamma }=y_1:C_1,\dots ,y_n:C_n$, transitively this includes the formation of every prefix and the judgment that each $C_k$ is a type in the preceding prefix. There are no further presuppositions.

The directly expanded Var instance is

For the type-formation instance of weakening, direct expansion gives

Finally, direct expansion of equality-respecting type substitution is

The underbraces mark every omitted entry and its supplier. Deleting those entries gives exactly the three compressed rules in the chapter.

The simultaneous context clause supplies $\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$. If $z:C$ occurs in $\mathrm{\Gamma }$, the same declaration occurs in the prefix of this enlarged context, so Assum immediately derives $\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢z:C$. Otherwise write $\mathrm{\Delta }={\mathrm{\Delta }}_1,z:C,{\mathrm{\Delta }}_2$. The context clause gives $\mathrm{\Gamma },x:A,{\mathrm{\Delta }}_1,z:C,{\mathrm{\Delta }}_2\mathsf{ctx}$; the declaration selected by the original rule is still present with the same type, and a second application of Assum gives the weakened judgment. Freshness of $x$ ensures that neither case changes the selected declaration or its type. The required context derivation is why context weakening and judgment weakening are proved simultaneously.

The componentwise composite is $$f\circ g=(b_1[c_1/u,c_2/v],b_2[c_1/u,c_2/v]).$$ The typing premises for $f$ include $$\mathrm{\Gamma },\mathrm{\Theta }⊢b_1:A,\mathrm{\Gamma },\mathrm{\Theta }⊢b_2:B(b_1).$$ Substitution by the telescope map $g$ in the second judgment gives $$\mathrm{\Gamma },\mathrm{\Xi }⊢b_2[c_1/u,c_2/v]:B(b_1[c_1/u,c_2/v]),$$ which is exactly the required type after the first composite component has been installed. Substitution in the first premise gives $\mathrm{\Gamma },\mathrm{\Xi }⊢b_1[c_1/u,c_2/v]:A$, because the target declaration $A$ is formed over $\mathrm{\Gamma }$ and contains no variable of $\mathrm{\Theta }$.

For $h:\mathrm{\Omega }{\Rightarrow }_{\mathrm{\Gamma }}\mathrm{\Xi }$, either association sends a component $b_i$ to $(b_i[g])[h]$. The structural-induction calculation in proposition 71.51 identifies this expression with $b_i[g\circ h]$. Hence every corresponding component is alpha-equivalent, so $(f\circ g)\circ h=f\circ (g\circ h)$ with the same substituted target types.

Unpack the two hypotheses. There are fresh names, say $r$ and $s$, such that $$e⟨r/x⟩{=}_{\alpha }f⟨r/y⟩,f⟨s/y⟩{=}_{\alpha }g⟨s/u⟩.$$ Choose one further name $t$ occurring in none of $e,f,g$ and distinct from $x,y,u,r,s$. Fresh-opening independence is used twice here: by proposition 26.7.1, the first displayed comparison remains true when its common opening $r$ is replaced by $t$, and the second remains true when $s$ is replaced by the same $t$. Hence $$e⟨t/x⟩{=}_{\alpha }f⟨t/y⟩{=}_{\alpha }g⟨t/u⟩.$$ Transitivity for the strictly smaller opened bodies gives $e⟨t/x⟩{=}_{\alpha }g⟨t/u⟩$. This is a common opening witnessing, by the operator clause in definition 26.6, $$L(x.e){=}_{\alpha }L(u.g).$$ Equivalently, rather than citing fresh-opening independence as a black box, one may open the first comparison successively at $r$ and $t$, use (26.1), and do the same with the second comparison. The only nonformal step is again the assertion that changing a fresh common opening does not change the alpha-comparison.

The displayed binder $y$ is not clean, because $y$ is free in the term being inserted. Choose distinct fresh names $r$ and $s$, both outside $\{x,y,z\}$. The two clean displays give respectively and To compare the two results, choose $t$ fresh for both. Their common openings are literally the same expression: $$P(P(y;z);r)⟨t/r⟩=P(P(y;z);t)=P(P(y;z);s)⟨t/s⟩.$$ Therefore $$L(r.P(P(y;z);r)){=}_{\alpha }L(s.P(P(y;z);s)).$$ The calculation also exhibits why the naive result $L(y.P(P(y;z);y))$ is wrong: it captures the free $y$ in the inserted copy of $P(y;z)$.

The displayed binder must first be freshened, since the letter $x$ is also the source variable of the substitution lemma. Choose $z$ outside $$\{x,y\}\cup \mathrm{FV}(a)\cup \mathrm{FV}(c)\cup \mathrm{FV}(a[c/y])$$ and write the unary expression as $L(z.e)$. Substitution passes through this clean binder, so the operator case is No binder is altered in this calculation because $z$ was chosen clean for all substituends.

The load-bearing side condition is $$x\notin \mathrm{FV}(c).$$ It is needed already in the variable case $e=y$: the two sides become $c$ and $c[a[c/y]/x]$, which agree precisely because substitution for $x$ leaves $c$ unchanged. Thus the term inserted for $y$ cannot reintroduce a free occurrence of $x$ that the later substitution would modify.

For the requested expression, choose the displayed binder $u$ outside all $\mathrm{FV}(a_i)$ and distinct from $x_1,x_2$. One-pass substitution gives $$P(x_1;L(u.P(x_2;u)))[a_1/x_1,a_2/x_2]=P(a_1;L(u.P(a_2;u))).$$ The iterated calculation is The second step does not alter the already inserted $a_1$, since $x_2\notin \mathrm{FV}(a_1)$.

For the general proof, choose one display of $e$ whose bound names avoid all source variables $x_i$ and all free variables of the $a_j$, and induct structurally on that display. At a variable $v$:

• if $v=x_i$, every substitution before the $i$-th leaves $v$ unchanged, the $i$-th replaces it by $a_i$, and every later substitution leaves $a_i$ unchanged because $x_j\notin \mathrm{FV}(a_i)$; both operations therefore return $a_i$;

• if $v\notin \{x_1,\dots ,x_n\}$, both operations leave $v$ unchanged.

At an operator $o({\overrightarrow{u}}_1.e_1;\dots ;{\overrightarrow{u}}_k.e_k)$, every substitution passes through each clean binder list. Apply the induction hypothesis to every body and reattach the same operator and binder lists. This proves $$e[a_1/x_1,\dots ,a_n/x_n]=e[a_1/x_1]\cdots [a_n/x_n].$$ The freshness assumptions are essential: without them, a later sequential substitution could rewrite a term inserted by an earlier one, whereas the simultaneous operation deliberately traverses each inserted term zero times.

Apply Subst first to the declaration $x:A$:

Here $y\notin \mathrm{FV}(a)$, so the declaration name survives and the new declaration really is $y:B[a/x]$. Now use the given typing judgment for $b$ as the first premise of a second substitution:

The declared variables of $\mathrm{\Delta }$ were chosen outside $\mathrm{FV}(a)\cup \mathrm{FV}(b)$, so both displayed telescope substitutions are defined. The second rule instance has ambient context $\mathrm{\Gamma }$, declaration type $B[a/x]$, and telescope $\mathrm{\Delta }[a/x]$, which is exactly why the premise for $b$ has the stated dependent type.

Write $\mathrm{\Gamma }=x_1:A_1,\dots ,x_n:A_n$. By proposition 26.25, derivability of $\mathrm{\Gamma },\mathrm{\Delta }\mathsf{ctx}$ is equivalent to the collection of all prefix typings for its declarations. Split that collection into two parts: $$x_1:A_1,\dots ,x_{k-1}:A_{k-1}⊢A_k\mathsf{type}(1\le k\le n)$$ and $$\mathrm{\Gamma },y_1:B_1,\dots ,y_{i-1}:B_{i-1}⊢B_i\mathsf{type}(1\le i\le m).$$ The same proposition says that the first group is equivalent to $\mathrm{\Gamma }\mathsf{ctx}$. Consequently the entire collection is equivalent to $\mathrm{\Gamma }\mathsf{ctx}$ together with every displayed typing judgment for $B_i$, as required.

For the reverse direction one may also see the construction directly: starting with $\mathrm{\Gamma }\mathsf{ctx}$, apply Ctx-Ext successively using the premises for $B_1,\dots ,B_m$. The forward direction repeatedly applies context inversion to the final context.

First substitute $a^{\prime }$ ordinarily into the given formation judgment:

The typing premise for $a^{\prime }$ is a presupposition of $\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$.

Context inversion of the original formation judgment gives $\mathrm{\Gamma },x:A⊢C\mathsf{type}$. Equal substitution with empty telescope then gives $$\mathrm{\Gamma }⊢C[a/x]\equiv C[a^{\prime }/x]\mathsf{type}.$$ Use Ty-Sym to orient this equality from the current declaration type to the desired one, and apply declaration conversion:

Thus $B[a^{\prime }/x]$ is formed in the common context based on $a$. Notice that the thesis is not substituted again during Ctx-Conv; only the type of the declaration $y$ changes.

Prove the following assertions simultaneously by rule induction:

1. if $x_1:A_1,\dots ,x_n:A_n\mathsf{ctx}$, then $$\mathrm{FV}(A_i)\subseteq \{x_1,\dots ,x_{i-1}\}(1\le i\le n);$$

2. if $\mathrm{\Gamma }⊢\mathcal{J}$, then the preceding property holds for $\mathrm{\Gamma }$ and $\mathrm{FV}(\mathcal{J})\subseteq \mathrm{dom}(\mathrm{\Gamma })$.

Here $\mathrm{FV}(\mathcal{J})$ includes every expression displayed in the thesis.

For Ctx-Emp there is nothing to prove. In Ctx-Ext, the induction hypothesis for $\mathrm{\Gamma }⊢A\mathsf{type}$ gives both the property for $\mathrm{\Gamma }$ and $\mathrm{FV}(A)\subseteq \mathrm{dom}(\mathrm{\Gamma })$, exactly the new final declaration condition.

Each presupposition rule is immediate. A rule that keeps the context merely discards some constituents of its premise thesis, so its free-variable set can only shrink. For Presup-Ext, the context induction hypothesis for $\mathrm{\Gamma },x:A$ directly says $\mathrm{FV}(A)\subseteq \mathrm{dom}(\mathrm{\Gamma })$. The reflexivity, symmetry, and transitivity rules for both equalities likewise retain or combine expressions already scoped in the same context; in transitivity the free-variable set of the conclusion is contained in the union of those of the two premises.

For Ctx-Conv, the equality premise gives $\mathrm{FV}(A^{\prime }),\mathrm{FV}(A)\subseteq \mathrm{dom}(\mathrm{\Gamma })$. The second induction hypothesis scopes every declaration in $\mathrm{\Delta }$ and the thesis in a context whose domain is $\mathrm{dom}(\mathrm{\Gamma })\cup \{x\}\cup \mathrm{dom}(\mathrm{\Delta })$. Replacing $A$ by $A^{\prime }$ changes no declared names and no expression in $\mathrm{\Delta }$ or $\mathcal{J}$, so all the same inclusions hold in the converted context.

For Subst, the premise induction hypotheses give $$\mathrm{FV}(a)\subseteq \mathrm{dom}(\mathrm{\Gamma }),\mathrm{FV}(E)\subseteq \mathrm{dom}(\mathrm{\Gamma })\cup \{x\}\cup \mathrm{dom}(\mathrm{\Delta })$$ for every declaration type or thesis constituent $E$ to the right of $x:A$. The free-variable formula for substitution therefore yields $$\mathrm{FV}(E[a/x])\subseteq \mathrm{dom}(\mathrm{\Gamma })\cup \mathrm{dom}(\mathrm{\Delta }),$$ which is the domain of $\mathrm{\Gamma },\mathrm{\Delta }[a/x]$. Applying this argument to each declaration type in order proves the context part as well. The two equal-substitution rules are identical except that both $a$ and $a^{\prime }$ occur in the conclusion; the equality premise scopes both in $\mathrm{\Gamma }$, so the same calculation applies to $E[a/x]$ and $E[a^{\prime }/x]$.

For Wk, the first premise scopes $A$ in $\mathrm{\Gamma }$. The second scopes $\mathrm{\Delta }$ and $\mathcal{J}$ in $\mathrm{\Gamma },\mathrm{\Delta }$; inserting the fresh name $x$ only enlarges every relevant prefix domain, while none of the old expressions acquires an occurrence of $x$. Hence the target context and thesis are scoped. For Var, the premise scopes $A$ in $\mathrm{\Gamma }$, and $$\mathrm{FV}(x:A)=\{x\}\cup \mathrm{FV}(A)\subseteq \mathrm{dom}(\mathrm{\Gamma },x:A).$$ These cases exhaust the structural rules.

An added type-former rule may be included only after verifying that every free variable in its conclusion occurs in a premise expression already scoped by the induction hypotheses, or is one of its declared local binders. No theorem is possible for an arbitrary added rule: for example, a rule $$\frac{\mathrm{\Gamma }\mathsf{ctx}}{\mathrm{\Gamma }⊢R(z)\mathsf{type}}$$ with $z\notin \mathrm{dom}(\mathrm{\Gamma })$ immediately derives a judgment violating the desired inclusion. Rule induction preserves properties supplied by the rules; it does not manufacture a missing scoping discipline out of optimism.

Let $${\mathcal{D}}_1:\mathrm{\Gamma }⊢a\equiv b:A,{\mathcal{D}}_2:\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}.$$ Restoring presuppositions gives $$\mathrm{\Gamma }⊢a:A,\mathrm{\Gamma }⊢b:A,\mathrm{\Gamma }⊢A\mathsf{type},\mathrm{\Gamma }⊢A^{\prime }\mathsf{type},\mathrm{\Gamma }\mathsf{ctx}.$$ The two term typings come from ${\mathcal{D}}_1$ and its symmetry via Presup-Eq-Tm; the two type formations come from ${\mathcal{D}}_2$ and its symmetry via Presup-Eq-Ty; the context follows by Presup-Ctx. Element conversion, already established in lemma 26.31, also supplies $$\mathrm{\Gamma }⊢a:A^{\prime },\mathrm{\Gamma }⊢b:A^{\prime },$$ which are the direct presuppositions of the desired conclusion.

Choose $x$ fresh. The generic-element branch, with its omitted premises restored, is

The last two displayed premises are the direct presuppositions of the target judgment and context; they are derived respectively by the type instance of Wk from $A\mathsf{type}$ and $A^{\prime }\mathsf{type}$, and by Ctx-Ext from $A\mathsf{type}$. The Ctx-Conv node is the precise point at which the declaration type of the generic element is converted from $A^{\prime }$ to $A$; the element remains classified by $A^{\prime }$.

Now apply the fully expanded equal-substitution instance with empty telescope:

The last four lines are exactly the direct and transitive presuppositions that are normally suppressed by convention 26.14. Substitution computes $x[a/x]=a$, $x[b/x]=b$, and $A^{\prime }[a/x]=A^{\prime }$ because $x$ was fresh.

Let the proposed permutation be represented by contexts $${\mathrm{\Gamma }}^{(0)}=\mathrm{\Gamma },{\mathrm{\Gamma }}^{(1)},\dots ,{\mathrm{\Gamma }}^{(k)}={\mathrm{\Gamma }}^{\prime },$$ where ${\mathrm{\Gamma }}^{(i+1)}$ is obtained from ${\mathrm{\Gamma }}^{(i)}$ by one certified adjacent swap. Induct on $i$. Suppose ${\mathrm{\Gamma }}^{(i)}⊢\mathcal{J}$ has been derived and write the relevant context as $${\mathrm{\Gamma }}^{(i)}={\mathrm{\Gamma }}_0,x:A,y:B,{\mathrm{\Gamma }}_1.$$ The certificate for this stage is a derivation ${\mathrm{\Gamma }}_0⊢B\mathsf{type}$. Apply Exch with telescope ${\mathrm{\Gamma }}_1$:

This is the required derivation in ${\mathrm{\Gamma }}^{(i+1)}$. Repeating the step $k$ times yields ${\mathrm{\Gamma }}^{\prime }⊢\mathcal{J}$. Each intermediate context is derivable as a presupposition of its transported judgment.

The test $x\notin \mathrm{FV}(B)$ is only a syntactic nonoccurrence test. It does not produce the typing derivation ${\mathrm{\Gamma }}_0⊢B\mathsf{type}$ required by Exch. In particular, $B$ could mention another undeclared name, fail to be a type for theory-specific reasons, or have been derivable in ${\mathrm{\Gamma }}_0,x:A$ only by a context-sensitive added rule for which no strengthening theorem is available. Removing a name from a free-variable set is not the same operation as removing a declaration from a derivation.

Put $${\mathrm{\Gamma }}_m={\mathrm{\Gamma }}_0,x:A,y_1:B_1,\dots ,y_m:B_m$$ and prove by induction on $m$ that ${\mathrm{\Gamma }}_m\mathsf{ctx}$ entails ${\mathrm{\Gamma }}_m⊢x:A$.

For $m=0$, Presup-Ext applied to ${\mathrm{\Gamma }}_0,x:A\mathsf{ctx}$ gives ${\mathrm{\Gamma }}_0⊢A\mathsf{type}$. Its own direct presupposition is ${\mathrm{\Gamma }}_0\mathsf{ctx}$. Hence the fully supplied Var instance is

where the final context premise is Ctx-Ext applied to the type premise. The extra lines are precisely what compression normally omits.

For the step, assume the result for $m$ and start from ${\mathrm{\Gamma }}_{m+1}\mathsf{ctx}$, where ${\mathrm{\Gamma }}_{m+1}={\mathrm{\Gamma }}_m,y_{m+1}:B_{m+1}$. Then Presup-Ext gives $${\mathrm{\Gamma }}_m⊢B_{m+1}\mathsf{type},$$ and repeated context peeling gives ${\mathrm{\Gamma }}_m\mathsf{ctx}$. The induction hypothesis gives ${\mathrm{\Gamma }}_m⊢x:A$. The relevant Wk instance, with empty telescope, is

Here ${\mathrm{\Gamma }}_m⊢A\mathsf{type}$ is Presup-Ty of the induction-hypothesis term judgment. The target context is Ctx-Ext applied to $B_{m+1}\mathsf{type}$. Finally, ${\mathrm{\Gamma }}_{m+1}⊢A\mathsf{type}$, the direct presupposition of the target term judgment, is the type-formation instance of Wk applied to $B_{m+1}\mathsf{type}$ and $A\mathsf{type}$. Thus every premise suppressed by convention 26.14 has a derivation at each step, completing the induction.

A fully premised typing scheme is

The last premise is the direct presupposition of the conclusion; it follows from the $Q$-formation rule but is displayed because the exercise asks for the full scheme.

For pointwise-equal parameters, take primed data satisfying $$\mathrm{\Gamma }⊢C\equiv C^{\prime }\mathsf{type},\mathrm{\Gamma },y:C⊢D\equiv D^{\prime }\mathsf{type},\mathrm{\Gamma },y:C^{\prime }⊢D^{\prime }\mathsf{type},$$ and term data satisfying $$\mathrm{\Gamma },y:C⊢d\equiv d^{\prime }:D,\mathrm{\Gamma },y:C^{\prime }⊢d^{\prime }:D^{\prime }.$$ In the equality judgments containing $D^{\prime }$ or $d^{\prime }$, the primed local context and classifier have first been transported to the unprimed ones using the earlier equalities. The formation congruence for $Q$ supplies $$\mathrm{\Gamma }⊢Q(C;y.D)\equiv Q(C^{\prime };y.D^{\prime })\mathsf{type}.$$ The term-congruence scheme, stated at the unprimed result type, is therefore

The final type-equality premise converts the primed constructor term from $Q(C^{\prime };y.D^{\prime })$ to the unprimed $Q(C;y.D)$, supplying the conclusion’s second term presupposition.

Now begin with an instance over $\mathrm{\Gamma },z:E$, a derivation $\mathrm{\Gamma }⊢a:E$, and choose $y\notin \mathrm{FV}(a)$. Structural stability under substitution gives

This is exactly the result of capture-avoiding substitution in every premise and in the conclusion.

The primitive rules of $T^{-}$ are handled as follows.

1. Ctx-Emp, Ctx-Ext, all type- and term-equality equivalence rules, and every added structurally stable scheme are also rules of $T$. A full-premise instance of an added rule is in particular an instance of its compressed $T$-form; surplus derivable presuppositions may simply be left unused.

2. Primitive Assum of $T^{-}$ is a derived rule of $T$ by lemma 26.34: context inversion extracts the declaration’s type, Var introduces the variable at that point, and successive Wk steps restore the suffix.

3. Primitive Conv of $T^{-}$ is derived in $T$ by lemma 26.31, using a fresh generic element, Ctx-Conv, and Subst.

4. Primitive Conv-Eq of $T^{-}$ is derived in $T$ by lemma 26.32, using the same converted generic element and Subst-Eq-Tm.

Thus every primitive $T^{-}$-rule has a finite $T$-derivation whose open leaves are exactly its premises.

Translate a whole $T^{-}$-derivation by induction on its proof tree. First translate all immediate premise subderivations. If the final rule is shared, reapply it. If it is Assum, Conv, or Conv-Eq, take the corresponding finite derived-rule tree above and graft the translated premise derivations into its open leaves. The result has the same conclusion as the original node. This explains why derivability is sufficient: proof trees are closed under such grafting, and no uniform derivation-transformation theorem beyond ordinary induction on the input tree is needed for this direction.

The first substitution removes $x:A$:

The second removes the transformed declaration of $y$:

The boxed premise is used precisely as the element premise of this second Subst instance; it could not have type $B$, because the first substitution has already changed the declaration. Under the freshness conditions in definition 26.45, the iterated result is the one-pass notation $\mathcal{J}[a/x,b/y]$.

The identity map would have components $(u,v)$. Its first component already violates the proposed side condition, since $u\in \mathrm{FV}(u)$ and $u$ is a target variable. Thus that definition excludes every nonempty identity map and cannot support the claimed unit law.

The repair is to keep $(u,v)$ as a legitimate relative map and rename only the target declarations in the derivation on which the map acts. With a fresh copy $\hat{\mathrm{\Delta }}=(\hat{u}:A,\hat{v}:B(\hat{u}))$, weaken the renamed derivation into the source context and substitute $u$ for $\hat{u}$, then $v$ for $\hat{v}$. Freshness now belongs to this auxiliary derivation, where it is obtainable by alpha-renaming, rather than to the map data, where identity makes it false.