Chapter 71Core route

The Rules of Dependent Type Theory

Consider a context $x : A, y : B (x) .$ The second declaration may use the first variable. Thus a context is not a bag of assumptions: its order carries mathematical information. Substituting an element $a : A$ must remove the declaration $x : A$ and simultaneously change $B (x)$ to $B (a)$ . The syntax and rules must make both operations exact while preserving the order on which the second operation depends.

Convention 71.1 — Ambient metatheory ¶

The metamathematics in this part is carried out in ZFC. In particular, raw expressions and derivation trees form sets, quotients are set-theoretic quotients, and induction on a least rule-closed collection is ordinary well-founded induction in the metatheory. Later model constructions state their additional size or large-cardinal hypotheses where those hypotheses are used; the syntactic arguments of this chapter use none of them.

Referenced from 3 locations

Raw syntax

Renaming the binder in $L (x . P (x; z))$ must change the bound occurrences of $x$ without changing the free occurrence of $z$ . A syntax tree must therefore record, for each argument of an operator, which variables that operator binds. A binding tree carries exactly this per-argument binding information.

Definition 26.1 — Binding trees ¶

Fix a countably infinite set $V$ of variables $x, y, z, \dots$ . Its infinitude guarantees that a variable outside any prescribed finite set of names can always be chosen.

A binding signature $Σ$ is a set of operators, each equipped with an arity: a finite list $(n_{1}, \dots, n_{k})$ of natural numbers. An operator of arity $(n_{1}, \dots, n_{k})$ takes $k$ arguments and binds $n_{i}$ variables in its $i$ -th argument.
The raw expressions over $Σ$ are generated inductively: every variable $x \in V$ is a raw expression; and if $o \in Σ$ has arity $(n_{1}, \dots, n_{k})$ , if $e_{1}, \dots, e_{k}$ are raw expressions, and if ${\vec{x}}_{i} = x_{i, 1}, \dots, x_{i, n_{i}}$ is a list of $n_{i}$ pairwise distinct variables for each $i$ , then $o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k})$ is a raw expression, in which the variables ${\vec{x}}_{i}$ are bound in $e_{i}$ .

Referenced from 11 locations

Example 26.2 — A running signature ¶

For the calculations in this section, take a constant $C$ of arity $()$ , a binary operator $P$ of arity $(0, 0)$ , and a unary binder $L$ of arity $(1)$ . Thus $P (C; x)$ and $L (x . P (x; z))$ are raw expressions. The second occurrence of $x$ in the latter expression is bound by $L$ ; the occurrence of $z$ is free. No typing meaning is assigned to $C, P, L$ . They are marks on which the binding operations can be seen.

Referenced from 2 locations

The Rules of Dependent Type Theory

Definition 26.3 — Names, size, and raw contexts ¶

The size, displayed bound names, and free variables of a raw expression are defined by $\begin{aligned} | x | & : = 1, & | o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k}) | & : = 1 + \sum_{i} | e_{i} |, \\ BN (x) & : = \emptyset, & BN (o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k})) & : = ⋃_{i} ({{\vec{x}}_{i}} \cup BN (e_{i})), \\ FV (x) & : = {x}, & FV (o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k})) & : = ⋃_{i} (FV (e_{i}) ∖ {{\vec{x}}_{i}}) . \end{aligned}$ A raw context is a finite list $x_{1} : A_{1}, \dots, x_{n} : A_{n}$ whose declared variables are pairwise distinct and whose $A_{i}$ are raw expressions. Write $dom (Γ)$ for its set of declared variables, $\cdot$ for the empty context, and $Γ, Δ$ for concatenation when the domains are disjoint. A raw context used to extend another is also called a telescope, a context extension whose later declaration types may use earlier declared variables.

Referenced from 3 locations

The Rules of Dependent Type Theory

For the running expression, $\begin{aligned} | L (x . P (x; z)) | & = 4, \\ BN (L (x . P (x; z))) & = {x}, & FV (L (x . P (x; z))) & = {z} . \end{aligned}$ The list $x : C, y : P (x; C)$ is a raw context. So is the reversed list $y : P (x; C), x : C$ : raw syntax has not yet enforced dependency order. The first list is derivably well formed only if $C$ is a type in the empty context and $P (x; C)$ is a type in the prefix $x : C$ . The reversed list fails this dependency test because $x$ is not declared in its first prefix.

Definition 26.4 — Fresh renaming ¶

Let $y$ occur nowhere in the raw expression $e$ . The fresh renaming $e ⟨ y / x ⟩$ replaces the free occurrences of $x$ by $y$ : $\begin{aligned} x ⟨ y / x ⟩ & : = y, \\ u ⟨ y / x ⟩ & : = u & (u \neq x), \\ o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k}) ⟨ y / x ⟩ & : = o ({\vec{x}}_{1} . e_{1}^{'}; \dots; {\vec{x}}_{k} . e_{k}^{'}), \end{aligned}$ where $e_{i}^{'} : = e_{i}$ if $x$ occurs in the binder list ${\vec{x}}_{i}$ , and $e_{i}^{'} : = e_{i} ⟨ y / x ⟩$ otherwise. Thus renaming stops when it reaches a binder for $x$ . Let the entries of each of $\vec{x}, \vec{y}$ be pairwise distinct, let the two sets of entries be disjoint, and let every target name in $\vec{y}$ occur nowhere in $e$ . We write $e ⟨ \vec{y} / \vec{x} ⟩$ for the successive renamings.

Referenced from 2 locations

The Rules of Dependent Type Theory

For $w$ fresh, the two possible behaviours are $\begin{aligned} L (x . P (x; z)) ⟨ w / z ⟩ & = L (x . P (x; w)), \\ L (x . P (x; z)) ⟨ w / x ⟩ & = L (x . P (x; z)) . \end{aligned}$ The second renaming stops at $L$ . By contrast, the body is a raw expression in which $x$ is free, so $P (x; z) ⟨ r / x ⟩ = P (r; z)$ . This last calculation is what permits us to compare two displayed binders.

Lemma 26.5 — Free variables after fresh renaming ¶

If $y$ occurs nowhere in $e$ , then $FV (e ⟨ y / x ⟩) = {\begin{cases} (FV (e) ∖ {x}) \cup {y}, & x \in FV (e), \\ FV (e), & x \notin FV (e) . \end{cases}$ Fresh renaming also preserves size; and if $x \notin FV (e)$ , then $e ⟨ y / x ⟩ = e$ .

Referenced from 5 locations

The Rules of Dependent Type Theory

Proof of Lemma 26.5 — Free variables after fresh renaming

Proof. Induct on $e$ . The two variable cases are the displayed alternatives. At $o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k})$ , renaming stops in precisely those arguments whose binder list contains $x$ . In every other argument apply the induction hypothesis, remove its binder list from the resulting free-variable set, and take the union over the arguments. Since $y$ occurs nowhere in the original expression, it belongs to no binder list. The same induction, with the defining equation for size, proves $| e ⟨ y / x ⟩ | = | e |$ . If $x$ is not free, a variable $z$ cannot equal $x$ , so $z ⟨ y / x ⟩ = z$ ; at an operator the renaming either stops at a binder for $x$ or the induction hypothesis leaves the body unchanged. This proves the final assertion. ◻

Definition 26.6 — α -equivalence ¶

The alpha-equivalence relation $=_{α}$ on raw expressions is generated inductively by the two clauses:

$x =_{α} x$ for every variable $x$ ;
$o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k}) =_{α} o ({\vec{y}}_{1} . f_{1}; \dots; {\vec{y}}_{k} . f_{k})$ (the same operator $o$ on both sides) whenever for each $i$ there is a list ${\vec{z}}_{i}$ of pairwise distinct variables, disjoint from ${\vec{x}}_{i}, {\vec{y}}_{i}$ and occurring in neither $e_{i}$ nor $f_{i}$ , such that $e_{i} ⟨ {\vec{z}}_{i} / {\vec{x}}_{i} ⟩ =_{α} f_{i} ⟨ {\vec{z}}_{i} / {\vec{y}}_{i} ⟩$ .

Referenced from 8 locations

Let $r$ occur nowhere in the displayed expressions. Opening both binders with $r$ gives the identical body $P (r; z)$ , and hence $L (x . P (x; z)) =_{α} L (y . P (y; z)) .$ The tempting expression $L (z . P (z; z))$ is not alpha-equivalent to either one: their common openings are $P (r; z)$ and $P (r; r)$ , which differ at the second variable. Renaming a binder to a free name is capture, not alpha-conversion.

Proposition 26.7 ¶

In clause 2 of definition 26.6, “for some fresh ${\vec{z}}_{i}$ ” may equivalently be replaced by “for every fresh ${\vec{z}}_{i}$ ”.
$=_{α}$ is an equivalence relation.
If $e =_{α} e^{'}$ then $FV (e) = FV (e^{'})$ .
If $e =_{α} e^{'}$ and the same fresh renaming is defined on both displays, then $e ⟨ \vec{w} / \vec{z} ⟩ =_{α} e^{'} ⟨ \vec{w} / \vec{z} ⟩$ .

Referenced from 6 locations

Proof of Proposition 26.7

Proof. We first record the raw calculation used in every clause. Let $\vec{x}, \vec{z}, \vec{w}$ have the same length, let the three lists be pairwise disjoint with distinct entries internally, and suppose $\vec{z}, \vec{w}$ occur nowhere in $e$ . Structural induction gives $e ⟨ \vec{z} / \vec{x} ⟩ ⟨ \vec{w} / \vec{z} ⟩ = e ⟨ \vec{w} / \vec{x} ⟩ .$ The variable case is immediate. At an operator, each renaming either stops at the argument’s binder list or passes into its body; in the latter case use the induction hypothesis for that body. The free-variable calculation needed below is lemma 26.5.

The companion commutation calculation is also needed. Let $z, w$ be distinct from one another and from the equally long, disjoint lists $\vec{x}, \vec{v}$ , suppose $\vec{v}, w$ occur nowhere in $e$ , and suppose $z \notin {\vec{x}}$ . Structural induction gives $e ⟨ \vec{v} / \vec{x} ⟩ ⟨ w / z ⟩ = e ⟨ w / z ⟩ ⟨ \vec{v} / \vec{x} ⟩ .$ At an operator both renamings stop or pass independently in each argument; when they pass, apply the induction hypothesis to that body.

Alpha-equivalent expressions have equal size. Indeed, rule induction on a derivation of $e =_{α} e^{'}$ shows $| e | = | e^{'} |$ . The variable clause is immediate. In the operator clause, the induction hypotheses say that every pair of common opened bodies has equal size; fresh renaming preserves size by lemma 26.5, so the corresponding original bodies have equal size. Both expressions use the same operator and arity, and the defining size equation therefore gives equal total sizes.

Complete induction on this common size proves four strengthened assertions simultaneously: independence of the fresh opening, compatibility with fresh renaming, the equivalence laws, and preservation of free variables. Every induction hypothesis below concerns an alpha-equivalent pair of strictly smaller common size.

Independence of the fresh opening. Suppose a common opening with ${\vec{z}}_{i}$ witnesses clause 2, and let ${\vec{w}}_{i}$ be any other allowable lists. The induction hypothesis for renaming compatibility renames the smaller related bodies from ${\vec{z}}_{i}$ to a third fresh list ${\vec{u}}_{i}$ . Equation (26.1) gives the same expressions as opening the original bodies directly at ${\vec{u}}_{i}$ . Repeat the renaming-compatibility step with ${\vec{u}}_{i}$ in place of ${\vec{z}}_{i}$ and ${\vec{w}}_{i}$ in place of ${\vec{u}}_{i}$ . Hence the comparison holds at every common fresh opening.

The later renaming step has the following exhaustive binder case split for one external name $z$ :

$z \in {{\vec{x}}_{i}}$	$z \in {{\vec{y}}_{i}}$	comparison after opening
no	no	commute both renamings by (26.2)
yes	yes	both external renamings stop at the binder
yes	no	free-variable preservation removes $z$ on the right after opening
no	yes	exchange the two displays in the preceding case

Compatibility with fresh renaming. It is enough to treat one renaming $⟨ w / z ⟩$ ; repeat the argument for a list. For an operator pair, fresh-opening independence permits common opening lists fresh for $z$ and $w$ . Consider one pair of corresponding arguments. If neither binder list contains $z$ , opening and the external renaming commute by (26.2); the induction hypothesis for renaming compatibility applies to the smaller opened bodies. If both binder lists contain $z$ , the external renaming stops on both sides, and the original common-opening comparison applies. Suppose, finally, that only one binder list contains $z$ . After that binder is opened at the fresh common list, $z$ is not free on that side. The induction hypothesis for free-variable preservation says it is not free on the other side either. On the side whose binder did not contain $z$ , the fresh-renaming formula implies $z \notin FV (f_{i})$ : opening at names disjoint from $z$ neither creates nor removes a free $z$ . Thus lemma 26.5 gives $f_{i} ⟨ w / z ⟩ = f_{i}$ before the opening. On the first side the external renaming stops at the binder. Both results are therefore the original common openings. Clause 2 of definition 26.6 rebuilds the operator and proves renaming compatibility. This case shows why one must prove, rather than assert, that an external renaming commutes with every opening.

Equivalence laws. Reflexivity is structural induction: at an operator choose fresh common openings and use reflexivity for the smaller opened bodies. Symmetry follows by reversing the comparisons in clause 2. For transitivity, suppose $\begin{aligned} o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k}) & =_{α} o ({\vec{y}}_{1} . f_{1}; \dots; {\vec{y}}_{k} . f_{k}), \\ o ({\vec{y}}_{1} . f_{1}; \dots; {\vec{y}}_{k} . f_{k}) & =_{α} o ({\vec{u}}_{1} . g_{1}; \dots; {\vec{u}}_{k} . g_{k}) . \end{aligned}$ Choose one list ${\vec{w}}_{i}$ fresh for all three $i$ -th bodies and disjoint from the three binder lists ${\vec{x}}_{i}, {\vec{y}}_{i}, {\vec{u}}_{i}$ . Fresh-opening independence opens both hypotheses with that same list. Transitivity for the smaller opened bodies, by the induction hypothesis, gives $e_{i} ⟨ {\vec{w}}_{i} / {\vec{x}}_{i} ⟩ =_{α} g_{i} ⟨ {\vec{w}}_{i} / {\vec{u}}_{i} ⟩;$ clause 2 rebuilds the operator.

Preservation of free variables. Variables are immediate. In the operator case, open the two $i$ -th bodies with one fresh list ${\vec{z}}_{i}$ . The induction hypothesis gives the exact equality $FV (e_{i} ⟨ {\vec{z}}_{i} / {\vec{x}}_{i} ⟩) = FV (f_{i} ⟨ {\vec{z}}_{i} / {\vec{y}}_{i} ⟩) .$ Remove the fresh variables ${\vec{z}}_{i}$ from this equality and use the fresh-renaming formula recorded above; the result is $FV (e_{i}) ∖ {{\vec{x}}_{i}} = FV (f_{i}) ∖ {{\vec{y}}_{i}} .$ Taking the union over $i$ is precisely the free-variable equation for the two operator expressions. ◻

Exercise 26.1 ¶

★☆☆ For an operator $L$ of arity $(1)$ , use two successive common openings to verify directly that $L (x . e) =_{α} L (y . f)$ and $L (y . f) =_{α} L (u . g)$ imply $L (x . e) =_{α} L (u . g)$ . Mark where fresh-opening independence is used.

Referenced from 3 locations

Convention 26.8 ¶

An expression is an alpha-equivalence class of raw expressions, and $=$ between expressions means $α$ -equivalence of representatives. To write an expression, choose a representative whose bound variables are pairwise distinct and distinct from all free variables in sight (the Barendregt convention). Raw contexts are not quotiented: the declared variables of a context are significant.

Referenced from 6 locations

Lemma 26.9 — Synchronized fresh displays ¶

Let $e =_{α} e^{'}$ and let $X$ be a finite set of variables. There are raw representatives $\bar{e} =_{α} e$ and ${\bar{e}}^{'} =_{α} e^{'}$ such that

corresponding operator arguments in $\bar{e}, {\bar{e}}^{'}$ use identical binder lists;
every bound name in either representative lies outside $X$ ;
corresponding bodies are alpha-equivalent.

In particular, every expression has a representative whose bound names avoid any prescribed finite set.

Referenced from 7 locations

Proof of Lemma 26.9 — Synchronized fresh displays

Proof. Use complete induction on size. Alpha-equivalent variables are the same variable, so there is nothing to choose. For operator expressions, choose for each pair of corresponding arguments one common binder list ${\vec{z}}_{i}$ outside $X$ , outside every name occurring in either body, and disjoint from the two original binder lists ${\vec{x}}_{i}, {\vec{y}}_{i}$ . This is permitted by proposition 26.7.1. The common openings $e_{i} ⟨ {\vec{z}}_{i} / {\vec{x}}_{i} ⟩ and f_{i} ⟨ {\vec{z}}_{i} / {\vec{y}}_{i} ⟩$ are alpha-equivalent and smaller than the original expressions. Apply the induction hypothesis to each pair, enlarging the forbidden set to include all the newly chosen ${\vec{z}}_{i}$ , and rebuild the operator with those common binder lists. For this rebuilding step, suppose ${\bar{p}}_{i} =_{α} e_{i} ⟨ {\vec{z}}_{i} / {\vec{x}}_{i} ⟩$ , open both proposed outer binders at a further fresh list ${\vec{u}}_{i}$ . Then ${\bar{p}}_{i} ⟨ {\vec{u}}_{i} / {\vec{z}}_{i} ⟩ \overset{p r o p o s i t i o n 26.7 .4}{=_{α}} e_{i} ⟨ {\vec{z}}_{i} / {\vec{x}}_{i} ⟩ ⟨ {\vec{u}}_{i} / {\vec{z}}_{i} ⟩ \overset{(26.1)}{=} e_{i} ⟨ {\vec{u}}_{i} / {\vec{x}}_{i} ⟩ .$ Clause 2 of definition 26.6 now shows that the rebuilt representative is alpha-equivalent to the original. Corresponding bodies remain alpha-equivalent by construction. Taking $e^{'} = e$ gives the final assertion. ◻

The need for a fresh representative is already visible with $L$ and $P$ . Replacing $x$ by $P (y; z)$ in $L (y . P (x; y))$ must not capture the inserted $y$ . With a naive recursion one would obtain $L (y . P (P (y; z); y)),$ where the first inserted $y$ has become bound. With a fresh $r$ , first choose the alpha-equivalent representative $L (r . P (x; r))$ ; capture-avoiding substitution gives $L (r . P (P (y; z); r)) .$

Definition 26.10 — Capture-avoiding substitution ¶

Let $e, a$ be expressions and $x$ a variable. Choose a representative of $e$ whose bound variables avoid $x$ and $FV (a)$ . The capture-avoiding substitution $e [a / x]$ is defined by recursion: $\begin{aligned} x [a / x] & : = a, & y [a / x] & : = y (y \neq x), \\ o ({\vec{x}}_{1} . e_{1}; \dots) [a / x] & : = o ({\vec{x}}_{1} . e_{1} [a / x]; \dots) . \end{aligned}$ More generally, let $x_{1}, \dots, x_{n}$ be pairwise distinct. Choose a display whose bound names avoid every $x_{i}$ and every $FV (a_{j})$ . The simultaneous substitution $e [a_{1} / x_{1}, \dots, a_{n} / x_{n}]$ is the recursion that sends a variable $x_{i}$ to $a_{i}$ , leaves every other variable fixed, and passes once through every operator argument. Thus an inserted $a_{i}$ is not subsequently changed by another entry of the same substitution. The synchronized-display argument in proposition 26.11.1 proves that this operation is independent of the chosen display and of the representatives of all $a_{i}$ . For a raw context $Δ = y_{1} : B_{1}, \dots, y_{m} : B_{m}$ whose declared variables avoid $x$ and $FV (a)$ we write $Δ [a / x] : = y_{1} : B_{1} [a / x], \dots, y_{m} : B_{m} [a / x]$ .

Referenced from 16 locations

For a deterministic named implementation one may fix $x_{0}, x_{1}, \dots$ and choose the least name outside the finite forbidden set. The mathematical operation remains the alpha-class specified above; proposition 26.11(1) proves independence from this choice.

Proposition 26.11 ¶

If $e =_{α} e^{'}$ and $a =_{α} a^{'}$ then $e [a / x] =_{α} e^{'} [a^{'} / x]$ ; substitution is well defined on expressions. More generally, simultaneous substitution is independent of the display of $e$ and of the representatives of all its substituends.
If $x \notin FV (e)$ then $e [a / x] = e$ .
$FV (e [a / x]) = (FV (e) ∖ {x}) \cup FV (a)$ if $x \in FV (e)$ , and $FV (e [a / x]) = FV (e)$ otherwise.
(Substitution lemma.) If $x \neq y$ and $x \notin FV (c)$ , then $e [a / x] [c / y] = e [c / y] [a [c / y] / x] .$
If $y$ occurs nowhere in $e$ , then ordinary substitution by the fresh variable coincides with fresh renaming: $e [y / x] = e ⟨ y / x ⟩$ .

Referenced from 9 locations

Proof of Proposition 26.11

Proof. For claim 1, proposition 26.7.3 gives $FV (a) = FV (a^{'})$ . Set $X = {x} \cup FV (a)$ . Apply lemma 26.9 to $e =_{α} e^{'}$ with forbidden set $X$ . We may therefore calculate with synchronized representatives whose corresponding binder lists are identical and safe for both inserted expressions. Structural induction on their common operator tree now proves $\bar{e} [a / x] =_{α} {\bar{e}}^{'} [a^{'} / x] .$ At a variable, the only nontrivial case is $x$ , where the assertion is $a =_{α} a^{'}$ . At an operator, apply the induction hypotheses to all corresponding bodies. To rebuild the common binder lists, open the two substituted bodies with one new list. Their alpha-equivalence is preserved by this fresh renaming by proposition 26.7.4, so clause 2 of definition 26.6 applies. This proves representative and substituend independence; no commutation of an opening with substitution is being assumed.

For simultaneous substitution, forbid all source variables and the union of the free-variable sets of all substituends, and apply lemma 26.9 once. The same induction on the synchronized operator trees has variable case $x_{i} \mapsto a_{i}$ and otherwise passes through each argument once. Reattachment is exactly the preceding argument. This proves the final assertion of claim 1.

Claims 2 and 3 are structural inductions on one clean representative. The variable cases are immediate. For $o ({\vec{x}}_{1} . e_{1}; \dots; {\vec{x}}_{k} . e_{k})$ , the binder names avoid $x$ and $FV (a)$ , so the induction hypotheses give $FV (e_{i} [a / x]) = {\begin{cases} (FV (e_{i}) ∖ {x}) \cup FV (a), & x \in FV (e_{i}), \\ FV (e_{i}), & x \notin FV (e_{i}) . \end{cases}$ Remove the argument’s binder list ${\vec{x}}_{i}$ and take the union over $i$ . Because those binders occur in neither ${x}$ nor $FV (a)$ , this is exactly claim 3. If $x$ is absent from the free variables of the whole operator expression, it is absent from every body after bound names are excluded; claim 2 follows from the body induction hypotheses.

For compatibility with substitution, the variable cases contain the reason for its side conditions. If $e = x$ : the left side is $x [a / x] [c / y] = a [c / y]$ , and the right side is $x [c / y] [a [c / y] / x] = x [a [c / y] / x] = a [c / y]$ , using $x \neq y$ . If $e = y$ : the left side is $y [a / x] [c / y] = y [c / y] = c$ , and the right side is $c [a [c / y] / x] = c$ by claim 2, since $x \notin FV (c)$ . If $e = z$ with $z \neq x, y$ , both sides are $z$ .

For the operator case put $X = {x, y} \cup FV (a) \cup FV (c) \cup FV (a [c / y])$ . Choose one representative of the outer expression whose bound names avoid $X$ . By lemma 26.9 and representative independence, choose representatives of $a$ and $c$ whose bound names also avoid $X$ . Every substitution below therefore passes through every binder in the chosen representatives. On the $i$ -th body the induction hypothesis gives $e_{i} [a / x] [c / y] = e_{i} [c / y] [a [c / y] / x] .$ Reattaching the unchanged operator and binder lists makes the left and right sides of claim 4 identical argument by argument. Claim 5 is the same structural induction: both operations send $x$ to $y$ , fix every other free variable, and pass through the common clean binder display. This completes the induction. ◻

Remark 26.12 ¶

We do not divide raw expressions into raw types and raw terms: the judgments of section 26.2 do the sorting. In a theory with a universe, one expression may itself be classified as a type, so a two-sorted raw grammar would have to be merged again. The signature is likewise open-ended: adding an operator does not change the uniform definitions of alpha-equivalence and substitution.

Referenced from 2 locations

The Rules of Dependent Type Theory

Exercise 26.2 ¶

★☆☆ Let $L$ have arity $(1)$ and $P$ arity $(0, 0)$ . With all displayed variables distinct, calculate $L (y . P (x; y)) [P (y; z) / x]$ from two different clean binder choices and verify their alpha-equivalence by common opening.

Referenced from 3 locations

Exercise 26.3 ¶

★☆☆ Specialize the substitution lemma to a unary binder $L (x . e)$ . Write the operator calculation in full and identify the hypothesis that prevents the term substituted for $y$ from reintroducing a free $x$ .

Referenced from 3 locations

Exercise 26.4 ¶

★★☆ Suppose $x_{i} \notin FV (a_{j})$ for all $i, j$ . Show that $e [a_{1} / x_{1}, \dots, a_{n} / x_{n}] = e [a_{1} / x_{1}] \dots [a_{n} / x_{n}] .$ First calculate both operations on $P (x_{1}; L (u . P (x_{2}; u)))$ for $n = 2$ and clean displayed binders; then prove the general statement by induction on an alpha-equivalent representative of $e$ whose bound variables avoid the substituted expressions.

Referenced from 3 locations

Judgments and contexts

Raw syntax cannot yet say that an expression is a type, that a term has a type, or that two of either are equal. Each assertion is relative to a context of typed variables, so five judgment forms are needed, not one.

Definition 26.13 — The judgment forms ¶

Dependent type theory has five judgment forms.

$Γ ctx$ — “ $Γ$ is a (well-formed) context.”
$Γ ⊢ A type$ — “ $A$ is a type in context $Γ$ .”
$Γ ⊢ a : A$ — “ $a$ is an element of type $A$ in context $Γ$ .”
$Γ ⊢ A \equiv B type$ — “ $A$ and $B$ are judgmentally equal types in context $Γ$ .”
$Γ ⊢ a \equiv b : A$ — “ $a$ and $b$ are judgmentally equal elements of type $A$ in context $Γ$ .”

Here $Γ$ is a raw context and $A, B, a, b$ are expressions. These notions were fixed in definition 26.1, definition 26.3, convention 26.8. The symbol $\equiv$ is reserved for judgmental equality throughout the book.

Referenced from 3 locations

Convention 26.14 — Presuppositions ¶

The presuppositions of a judgment form are the well-formedness obligations of its parts listed below:

judgment	presupposes
$Γ, x : A ctx$	$Γ ctx$ and $Γ ⊢ A type$
$Γ ⊢ A type$	$Γ ctx$
$Γ ⊢ a : A$	$Γ ⊢ A type$
$Γ ⊢ A \equiv B type$	$Γ ⊢ A type$ and $Γ ⊢ B type$
$Γ ⊢ a \equiv b : A$	$Γ ⊢ a : A$ and $Γ ⊢ b : A$

(and, transitively, everything these presuppose). The first row is recursive; the empty context has no presupposition. We adopt two disciplines. (i) Asserting a judgment, in prose or as the premise of a rule, implicitly asserts its presuppositions. (ii) In displayed rules we compress premises: a premise is omitted when its derivability follows from the presuppositions of the displayed premises and conclusion. This convention is cited by number whenever compression is used.

Referenced from 34 locations

The structural rules

The five judgment forms are generated simultaneously. Context extension requires a type in the preceding context, so context formation and type formation cannot be defined independently. An extension $Γ, x : A$ is always a raw context, so $x \notin dom (Γ)$ .

Definition 26.15 — Contexts and presuppositions ¶

Context formation is governed by

\cdot ctx

Ctx-Emp

Γ ⊢ A type

Γ, x : A ctx

Ctx-Ext

Each judgment also yields its direct presuppositions:

Γ ⊢ A type

Γ ctx

Presup-Ctx

Γ, x : A ctx

Γ ⊢ A type

Presup-Ext

Γ ⊢ a : A

Γ ⊢ A type

Presup-Ty

Γ ⊢ A \equiv B type

Γ ⊢ A type

Presup-Eq-Ty

Γ ⊢ a \equiv b : A

Γ ⊢ a : A

Presup-Eq-Tm

Referenced from 2 locations

The Rules of Dependent Type Theory

The rule Ctx-Emp is a complete derivation of $\cdot ctx$ . Given a derivation $D$ of $\cdot ⊢ A type$ , Ctx-Ext forms the one-declaration context:

D : \cdot ⊢ A type

x : A ctx

Ctx-Ext

Conversely, Presup-Ext extracts the same type-formation judgment from any derivation of $x : A ctx$ . Context extension and context inversion are thus two visible operations, not two implicit side conditions.

Definition 26.16 — Equality rules ¶

Judgmental equality is an equivalence relation, separately for types and for elements:

Γ ⊢ A type

Γ ⊢ A \equiv A type

Ty-Refl

Γ ⊢ A \equiv B type

Γ ⊢ B \equiv A type

Ty-Sym

Γ ⊢ A \equiv B type

Γ ⊢ B \equiv C type

Γ ⊢ A \equiv C type

Ty-Trans

Γ ⊢ a : A

Γ ⊢ a \equiv a : A

Tm-Refl

Γ ⊢ a \equiv b : A

Γ ⊢ b \equiv a : A

Tm-Sym

Γ ⊢ a \equiv b : A

Γ ⊢ b \equiv c : A

Γ ⊢ a \equiv c : A

Tm-Trans

Referenced from 5 locations

For example, from $a \equiv b : A$ and $c \equiv b : A$ we obtain $a \equiv b : A, b \equiv c : A ⟹ a \equiv c : A,$ first by Tm-Sym on the second judgment and then by Tm-Trans. The type-equality calculation is identical with the prefix Ty-.

Convention 26.17 — Generic judgment theses ¶

The letter $J$ ranges over the four judgment theses, the parts of an expression judgment that follow its context: $A type, A \equiv B type, a : A, a \equiv b : A .$ Thus $Γ ⊢ J$ abbreviates four judgments. Substitution in $J$ acts on every constituent expression, and $FV (J)$ is the union of their free-variable sets.

Referenced from 3 locations

Definition 26.18 — Conversion of a declaration ¶

The type of a declared variable may be replaced by a judgmentally equal type:

Γ ⊢ A \equiv A^{'} type

Γ, x : A, Δ ⊢ J

Γ, x : A^{'}, Δ ⊢ J

Ctx-Conv

The rule acts on every thesis abbreviated by $J$ . Its first premise is indispensable: changing a declaration to a merely well-formed, but unequal, type would change the mathematical assumption.

Referenced from 2 locations

The Rules of Dependent Type Theory

For example, if $Γ ⊢ A \equiv A^{'} type$ and $Γ, x : A ⊢ x : A$ , context conversion followed by term conversion gives $\frac{\begin{matrix} Γ ⊢ A \equiv A^{'} type \\ Γ, x : A ⊢ x : A \end{matrix}}{Γ, x : A^{'} ⊢ x : A} Ctx - Conv, Γ, x : A^{'} ⊢ x : A^{'} .$ Without $A \equiv A^{'}$ , the putative conclusion could assert $x : 2 ⊢ x : N$ merely because both declaration types are formed; no structural rule can supply that judgment.

Definition 26.19 — Families and sections ¶

Let $Γ ⊢ A type$ . A family of types over $A$ is a type $Γ, x : A ⊢ B type$ , and a section is an element $Γ, x : A ⊢ b : B$ . For $Γ ⊢ a : A$ , the expression $B [a / x]$ is the fiber at $a$ . We also write $B (x)$ for the family and $B (a)$ for the fiber, and set $b (a) : = b [a / x]$ .

Referenced from 2 locations

The Rules of Dependent Type Theory

Definition 26.20 — Substitution rules ¶

Substitution removes a declaration by replacing its variable with an element:

Γ ⊢ a : A

Γ, x : A, Δ ⊢ J

Γ, Δ [a / x] ⊢ J [a / x]

Subst

Γ ⊢ a \equiv a^{'} : A

Γ, x : A, Δ ⊢ B type

Γ, Δ [a / x] ⊢ B [a / x] \equiv B [a^{'} / x] type

Subst-Eq-Ty

Γ ⊢ a \equiv a^{'} : A

Γ, x : A, Δ ⊢ b : B

Γ, Δ [a / x] ⊢ b [a / x] \equiv b [a^{'} / x] : B [a / x]

Subst-Eq-Tm

In these schemes the declared names of $Δ$ are chosen outside $FV (a)$ , and outside $FV (a^{'})$ in the two equality schemes, so every displayed context substitution is defined as in definition 26.10. The first rule acts on all four theses. The other two say that substituting equal elements gives equal types and equal terms in the common context obtained with $a$ .

Referenced from 3 locations

Here is the basic calculation. Given an element and a family,

Γ ⊢ a : A

Γ, x : A ⊢ B type

Γ ⊢ B [a / x] type

Subst

derives the fiber. With a telescope $y : B$ to the right, the same rule changes both the declaration and the thesis: $Γ, x : A, y : B ⊢ J ⟶ Γ, y : B [a / x] ⊢ J [a / x] .$

Exercise 26.5 ¶

★☆☆ Derive the two-variable substitution rule: from $Γ ⊢ a : A$ , $Γ ⊢ b : B [a / x]$ , and $Γ, x : A, y : B, Δ ⊢ J$ , conclude $Γ, Δ [a / x] [b / y] ⊢ J [a / x] [b / y]$ . Choose the declared names of $Δ$ outside $FV (a) \cup FV (b)$ and choose $y \notin FV (a)$ , so all displayed context substitutions are defined.

Referenced from 3 locations

Definition 26.21 — Weakening and the generic element ¶

Weakening inserts an unused declaration, while the variable rule gives the element named by a final declaration:

Γ ⊢ A type

Γ, Δ ⊢ J

Γ, x : A, Δ ⊢ J

Γ ⊢ A type

Γ, x : A ⊢ x : A

Var

Referenced from 4 locations

Choose $x$ fresh for $B$ . From $Γ ⊢ A type$ and $Γ ⊢ B type$ , weakening produces the constant family

Γ ⊢ A type

Γ ⊢ B type

Γ, x : A ⊢ B type

Its fiber at $a : A$ is $B [a / x] = B$ . In contrast, Var produces the section $Γ, x : A ⊢ x : A$ whose value after substituting $a$ is the element $a$ itself.

Definition 26.22 — The structural rules ¶

The context, equality, declaration-conversion, substitution, weakening, and variable rules just displayed are collectively called the structural rules. Their premises are compressed according to convention 26.14.

Referenced from 23 locations

Remark 26.23 — Simultaneity ¶

The five judgments are the least classes closed under all structural rules and under the chosen formation, introduction, elimination, and equality rules. They are generated simultaneously because Ctx-Ext has a type judgment as its premise and a context judgment as its conclusion. Rule induction over this simultaneous generation proves one property for each of the five judgment forms (theorem 1.15).

Referenced from 4 locations

Proposition 26.24 — Sanity ¶

If a judgment is derivable, so are all of its presuppositions in the sense of convention 26.14; in particular, if $Γ ⊢ J$ is derivable then so is $Γ ctx$ .

Referenced from 3 locations

The Rules of Dependent Type Theory

Proof of Proposition 26.24 — Sanity

Proof. Use the presupposition and equality rules. From $Γ ⊢ a : A$ , Presup-Ty gives $Γ ⊢ A type$ , and then Presup-Ctx gives $Γ ctx$ . From $Γ ⊢ A \equiv B type$ , Presup-Eq-Ty gives $Γ ⊢ A type$ ; composing Ty-Sym with Presup-Eq-Ty gives $Γ ⊢ B type$ ; and Presup-Ctx gives $Γ ctx$ . From $Γ ⊢ a \equiv b : A$ , Presup-Eq-Tm gives $Γ ⊢ a : A$ , composing Tm-Sym with Presup-Eq-Tm gives $Γ ⊢ b : A$ , and the previous case finishes. From $Γ ⊢ A type$ , Presup-Ctx gives $Γ ctx$ . Finally, from $Γ, x : A ctx$ , Presup-Ext gives $Γ ⊢ A type$ and then Presup-Ctx gives $Γ ctx$ . Iterating these five derivations establishes every transitive presupposition in convention 26.14. ◻

Proposition 26.25 — Characterization of contexts ¶

Assume that no added rule concludes a context judgment and that every added rule has, among its full premises, the context judgment presupposed by its conclusion. Let $Γ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ be a raw context. The judgment $Γ ctx$ is derivable if and only if for each $1 \leq k \leq n$ the judgment $x_{1} : A_{1}, \dots, x_{k - 1} : A_{k - 1} ⊢ A_{k} type$ is derivable.

Referenced from 7 locations

Proof of Proposition 26.25 — Characterization of contexts

Proof. ( $\Leftarrow$ ) For $n = 0$ apply Ctx-Emp; for $n \geq 1$ apply Ctx-Ext to the $k = n$ judgment.

( $\Rightarrow$ ) We prove two assertions simultaneously by rule induction. If $Γ ctx$ is derivable, every declaration of $Γ$ has a derivable type judgment in its preceding prefix. If $Γ ⊢ J$ is derivable, the same prefix property holds for its ambient context $Γ$ . We treat each structural rule and then the added rules.

For Ctx-Emp the assertion is empty. For Ctx-Ext, the premise is $x_{1} : A_{1}, \dots, x_{n - 1} : A_{n - 1} ⊢ A_{n} type$ ; the inductive hypothesis for it yields the type judgments for all $k < n$ , and the premise itself is the case $k = n$ .

Every presupposition rule either keeps the context or removes its last declaration. In the first case its premise induction hypothesis is exactly the desired prefix property; in the second, Presup-Ext, take the proper prefixes established for $Γ, x : A$ . Each equality rule has a premise in the same context as its conclusion, so its induction hypothesis applies unchanged.

For Ctx-Conv, suppose the conclusion context is $Γ, x : A^{'}, Δ$ . From the equality premise $Γ ⊢ A \equiv A^{'} type$ , rule Ty-Sym gives $Γ ⊢ A^{'} \equiv A type$ , and Presup-Eq-Ty then gives $Γ ⊢ A^{'} type$ . Fix a prefix $Δ^{'}$ of $Δ$ whose following declaration is $y : B$ . The induction hypothesis for the judgment premise gives $Γ, x : A, Δ^{'} ⊢ B type .$ Apply Ctx-Conv with the same equality premise to derive $Γ, x : A^{'}, Δ^{'} ⊢ B type$ . Prefixes wholly inside $Γ$ come from the equality premise’s induction hypothesis.

For Subst, from $Γ ⊢ a : A$ and $Γ, x : A, Δ ⊢ J$ , prefixes of $Γ$ come from the first induction hypothesis. For a prefix reaching into $Δ [a / x]$ , with next type $B [a / x]$ , the second induction hypothesis gives $Γ, x : A, Δ^{'} ⊢ B type$ ; one application of Subst gives $Γ, Δ^{'} [a / x] ⊢ B [a / x] type$ . For Subst-Eq-Ty, apply Subst to both type premises with substitution $[a / x]$ ; for Subst-Eq-Tm, apply it to the common classifier premise. Both yield the displayed conclusion context $Γ, Δ^{'} [a / x]$ .

For Wk, from $Γ ⊢ A type$ and $Γ, Δ ⊢ J$ to $Γ, x : A, Δ ⊢ J$ . The prefixes of $Γ$ are handled by the inductive hypothesis of the first premise, the prefix ending in $A$ by the first premise itself. For a prefix reaching into $Δ$ , say with next type $B$ , the inductive hypothesis of the second premise gives $Γ, Δ^{'} ⊢ B type$ for the corresponding prefix $Δ^{'}$ of $Δ$ , and one application of Wk (with the first premise) gives $Γ, x : A, Δ^{'} ⊢ B type$ .

For Var, the type premise gives all prefixes of $Γ$ by its inductive hypothesis and gives the final declaration type $A$ itself. Finally, an added rule cannot conclude a context judgment. For its non-context conclusion, the hypothesis of the proposition gives a context premise for the conclusion context. Its induction hypothesis gives the prefix property. These cases exhaust the simultaneous rule set. ◻

Corollary 26.26 — Context inversion ¶

Under the hypotheses on added rules in proposition 26.25, if $Γ, x : A, Δ ctx$ is derivable, then so are $Γ ctx$ and $Γ ⊢ A type$ . More generally the same follows, via proposition 26.24, from any derivable judgment $Γ, x : A, Δ ⊢ J$ .

Referenced from 2 locations

The Rules of Dependent Type Theory

Proof of Corollary 26.26 — Context inversion

Proof. The prefix property of proposition 26.25 gives $Γ ⊢ A type$ directly, and Presup-Ctx gives $Γ ctx$ . ◻

Lemma 26.27 — The common context for equal substitution ¶

Assume both hypotheses on added rules in proposition 26.25. Let $Γ ⊢ a \equiv a^{'} : A$ and let $Γ, x : A, Δ ⊢ J$ . Then both $Γ, Δ [a / x] ⊢ J [a / x] and Γ, Δ [a / x] ⊢ J [a^{'} / x]$ are derivable. In the second judgment every declared type and every constituent of $J$ is substituted with $a^{'}$ , but the displayed context is the one obtained with $a$ .

Referenced from 2 locations

The Rules of Dependent Type Theory

Proof of Lemma 26.27 — The common context for equal substitution

Proof. The first judgment is Subst. Ordinary substitution with $a^{'}$ gives the second thesis over $Γ, Δ [a^{'} / x]$ ; we convert that context one declaration at a time. Write $Δ = y_{1} : B_{1}, \dots, y_{m} : B_{m}$ , and let $Δ_{i - 1}$ denote its first $i - 1$ declarations. Suppose those declarations have already been converted from their $a^{'}$ -forms to their $a$ -forms. Context inversion applied before substitution gives $Γ, x : A, y_{1} : B_{1}, \dots, y_{i - 1} : B_{i - 1} ⊢ B_{i} type .$ The rule Subst-Eq-Ty, instantiated with the telescope $Δ_{i - 1}$ , gives directly $Γ, Δ_{i - 1} [a / x] ⊢ B_{i} [a / x] \equiv B_{i} [a^{'} / x] type .$ Apply Ty-Sym, then Ctx-Conv at the $i$ -th declaration: the context being transported currently contains $B_{i} [a^{'} / x]$ , and the desired context contains $B_{i} [a / x]$ . Induction on $i$ converts the whole telescope and transports the thesis to the common context. The case $m = 0$ requires no conversion. ◻

Remark 26.28 ¶

In the absence of type formers the structural rules generate exactly one derivable judgment, namely $\cdot ctx$ : every other rule has a premise requiring some type to exist. Any type-formation axiom populates the calculus.

Referenced from 2 locations

The Rules of Dependent Type Theory

Exercise 26.6 ¶

★☆☆ List all direct and transitive presuppositions of $Γ, x : A ⊢ a \equiv b : B$ . Include the presuppositions of the nonempty context itself.

Referenced from 3 locations

Exercise 26.7 ¶

★★☆ Call a rule instance directly expanded when it explicitly lists the displayed premises and every direct presupposition of those premises and the conclusion; do not recursively expand the resulting context judgments. Directly expand Var, the type-formation instance of Wk, and Subst-Eq-Ty. Mark each entry omitted under convention 26.14 and the premise or conclusion that supplies it.

Referenced from 3 locations

Exercise 26.8 ¶

★☆☆ Let $Δ = y_{1} : B_{1}, \dots, y_{m} : B_{m}$ . Deduce from proposition 26.25 that $Γ, Δ ctx$ is derivable exactly when $Γ ctx$ and every $Γ, y_{1} : B_{1}, \dots, y_{i - 1} : B_{i - 1} ⊢ B_{i} type$ are derivable.

Referenced from 3 locations

Exercise 26.9 ¶

★★☆ Take $Δ = y : C$ . Starting from $Γ ⊢ a \equiv a^{'} : A$ and $Γ, x : A, y : C ⊢ B type$ , write the context-conversion calculation that types $B [a^{'} / x]$ in the common context $Γ, y : C [a / x]$ .

Referenced from 3 locations

Exercise 26.10 ¶

★★★ Set up the simultaneous induction that will apply after type-former rules are added, and verify for each structural-rule case that $Γ ⊢ J$ would imply $FV (J) \subseteq dom (Γ)$ and that, in a derivable context, each declared type has free variables only among earlier declarations. The empty structural theory has no non-context example, so these are induction steps rather than a nonvacuous closed theorem. An added type-former rule may be included in the induction only after checking the same scoping property for that rule; explain why no conclusion is possible for an arbitrary added rule.

Referenced from 3 locations

Example derivations

Everyday derivations use renaming, exchange, general variables, and the two conversion rules as single steps. Each must first be derived from the primitive structural rules. Recall that a rule is derivable when its conclusion has a derivation from its premises taken as axioms (definition 1.32).

Remark 26.29 ¶

Expressions in a judgment are alpha-classes, but a judgment is not quotiented by renaming variables declared in its context: those variables occur free in the declarations and thesis to their right. Such a change is a derivation, not an identification. The following lemma constructs it.

Referenced from 2 locations

The Rules of Dependent Type Theory

Lemma 71.31 — Context peeling ¶

From a hypothesis axiom $Γ, x : A, Δ ⊢ J$ , derive both $Γ, x : A, Δ ctx$ and $Γ ⊢ A type$ .

Referenced from 4 locations

The Rules of Dependent Type Theory

Proof of Lemma 71.31 — Context peeling

Proof. A type thesis uses Presup-Ctx; a term thesis uses Presup-Ty and then Presup-Ctx; a type equality uses Presup-Eq-Ty and then Presup-Ctx; and a term equality uses Presup-Eq-Tm, Presup-Ty, and Presup-Ctx. These cases derive $Γ, x : A, Δ ctx$ . Repeatedly apply Presup-Ext followed by Presup-Ctx to peel the declarations of $Δ$ ; one final Presup-Ext derives $Γ ⊢ A type$ . Every step is a node over the original hypothesis axiom, so the calculation is valid in hypothetical derivability. ◻

Lemma 26.30 — Change of variables ¶

Let $x^{'}$ be a variable occurring nowhere in the judgment $Γ, x : A, Δ ⊢ J$ . Then the rule

Γ, x : A, Δ ⊢ J

Γ, x^{'} : A, Δ [x^{'} / x] ⊢ J [x^{'} / x]

Rename

is derivable.

Referenced from 4 locations

Proof of Lemma 26.30 — Change of variables

Proof. Apply lemma 71.31 to the premise and call the resulting derivation of $Γ ⊢ A type$ by $D$ . Then

Γ ⊢ A type

Γ, x^{'} : A ⊢ x^{'} : A

Var

Γ ⊢ A type

Γ, x : A, Δ ⊢ J

Γ, x^{'} : A, x : A, Δ ⊢ J

Γ, x^{'} : A, Δ [x^{'} / x] ⊢ J [x^{'} / x]

Subst

where both undischarged leaves $Γ ⊢ A type$ stand for $D$ . The final step is the instance of Subst with ambient context $Γ, x^{'} : A$ , substituted element $x^{'}$ , and telescope $Δ$ ; its side conditions hold since $x^{'}$ is globally fresh. ◻

Lemma 71.33 — Substitute while retaining the source declaration ¶

If $Γ ⊢ a : A$ and $Γ, x : A, Δ ⊢ J$ , then $Γ, x : A, Δ [a / x] ⊢ J [a / x] .$ For context formation, the corresponding conclusion is $Γ, x : A, Δ [a / x] ctx$ whenever $Γ, x : A, Δ ctx$ .

Referenced from 2 locations

The Rules of Dependent Type Theory

Proof of Lemma 71.33 — Substitute while retaining the source declaration

Proof. Apply Subst to obtain $Γ, Δ [a / x] ⊢ J [a / x]$ . Because $a$ is typed in $Γ$ , the result contains no free $x$ . Apply Wk at the cut after $Γ$ to reinsert $x : A$ . For context formation, induct on $Δ$ . After Subst forms the next declaration over $Γ, Δ^{'} [a / x]$ , Wk reinserts $x : A$ at the cut after $Γ$ , and Ctx-Ext appends that declaration to $Γ, x : A, Δ^{'} [a / x]$ . ◻

Lemma 26.31 — Element conversion ¶

The rule

Γ ⊢ a : A

Γ ⊢ A \equiv A^{'} type

Γ ⊢ a : A^{'}

Conv

is derivable.

Referenced from 7 locations

Proof of Lemma 26.31 — Element conversion

Proof. From the second premise, $Γ ⊢ A^{'} type$ is derivable by Ty-Sym and Presup-Eq-Ty. Choose $x$ to occur nowhere in $Γ, A, A^{'}, a$ . Then $x \notin FV (A^{'})$ , so $A^{'} [a / x] = A^{'}$ , and the tree

Γ ⊢ a : A

Γ ⊢ A \equiv A^{'} type

Γ ⊢ A^{'} \equiv A type

Ty-Sym

Γ ⊢ A^{'} type

Γ, x : A^{'} ⊢ x : A^{'}

Var

Γ, x : A ⊢ x : A^{'}

Ctx-Conv

Γ ⊢ a : A^{'}

Subst

derives the conclusion: the Ctx-Conv step converts the context entry $x : A^{'}$ to $x : A$ along $Γ ⊢ A^{'} \equiv A type$ , and the final Subst step substitutes $a$ for $x$ in the thesis $x : A^{'}$ . Implementations usually reverse this presentation choice: Conv is a primitive kernel rule, while the more global context-conversion operation is proved admissible. ◻

Lemma 26.32 — Equality conversion ¶

The rule

Γ ⊢ a \equiv b : A

Γ ⊢ A \equiv A^{'} type

Γ ⊢ a \equiv b : A^{'}

Conv-Eq

is derivable.

Referenced from 7 locations

Proof of Lemma 26.32 — Equality conversion

Proof. Choose $x$ to occur nowhere in $Γ, A, A^{'}, a, b$ . The proof repeats the useful part of element conversion. Symmetry of the second premise and Ctx-Conv turn the generic element at $A^{'}$ into $Γ, x : A ⊢ x : A^{'} .$ Now use the first premise in Subst-Eq-Tm, with empty telescope and with the displayed judgment as its second premise:

Γ ⊢ a \equiv b : A

Γ ⊢ A \equiv A^{'} type

Γ ⊢ A^{'} \equiv A type

Ty-Sym

Γ ⊢ A^{'} type

Γ, x : A^{'} ⊢ x : A^{'}

Var

Γ, x : A ⊢ x : A^{'}

Ctx-Conv

Γ ⊢ a \equiv b : A^{'}

Subst-Eq-Tm

The omitted formation leaf $Γ ⊢ A^{'} type$ is the presupposition of $Γ ⊢ A \equiv A^{'} type$ . ◻

Exercise 26.11 ¶

★★☆ Reconstruct the derivation of lemma 26.32 with every presupposition premise restored, and mark the point at which the type of the generic element is converted.

Referenced from 3 locations

Lemma 26.33 — Interchange ¶

The rule

Γ ⊢ B type

Γ, x : A, y : B, Δ ⊢ J

Γ, y : B, x : A, Δ ⊢ J

Exch

is derivable. (The premise $Γ ⊢ B type$ records that $B$ does not depend on $x$ .)

Referenced from 3 locations

Proof of Lemma 26.33 — Interchange

Proof. Let $y^{'}$ be globally fresh, and obtain $Γ ⊢ A type$ from the second premise by lemma 71.31. Rename $y$ to $y^{'}$ , weaken by $y : B$ in the correct position, and then substitute $y$ for $y^{'}$ . Formally,

Γ ⊢ B type

Γ ⊢ A type

Γ, y : B ⊢ A type

Γ ⊢ B type

Γ, y : B ⊢ y : B

Var

Γ, y : B, x : A ⊢ y : B

Γ ⊢ B type

Γ, x : A, y : B, Δ ⊢ J

Γ, x : A, y^{'} : B, Δ [y^{'} / y] ⊢ J [y^{'} / y]

Rename

Γ, y : B, x : A, y^{'} : B, Δ [y^{'} / y] ⊢ J [y^{'} / y]

Γ, y : B, x : A, Δ ⊢ J

Subst

In the left branch, the inner Wk inserts $y : B$ under $A$ , and the outer Wk appends $x : A$ ; in the right branch, Wk inserts $y : B$ between $Γ$ and $x : A$ . The final Subst substitutes $y$ for $y^{'}$ ; since $y^{'}$ is fresh, $Δ [y^{'} / y] [y / y^{'}] = Δ$ and $J [y^{'} / y] [y / y^{'}] = J$ . ◻

Exercise 26.12 ¶

★★☆ Call two adjacent declarations in $Γ_{0}, x : A, y : B, Γ_{1}$ swappable when $Γ_{0} ⊢ B type$ is derivable. Suppose a permutation of a derivable context is presented as a sequence of adjacent swaps, and each swap is swappable in the context reached at that stage. Use Exch at every stage to transport a derivation of $Γ ⊢ J$ to the permuted context. Why would the weaker syntactic test $x \notin FV (B)$ be insufficient?

Referenced from 3 locations

Lemma 26.34 — General variable rule ¶

The rule

Γ ctx

(x : A) \in Γ

Γ ⊢ x : A

Assum

is derivable, where $(x : A) \in Γ$ is the side condition that the declaration $x : A$ occurs in $Γ$ .

Referenced from 8 locations

Proof of Lemma 26.34 — General variable rule

Proof. Write $Γ = Γ_{0}, x : A, y_{1} : B_{1}, \dots, y_{m} : B_{m}$ . By repeated primitive Presup-Ext and Presup-Ctx steps applied to the context premise, the judgments $Γ_{0} ⊢ A type$ and $Γ_{0}, x : A, y_{1} : B_{1}, \dots, y_{j - 1} : B_{j - 1} ⊢ B_{j} type$ ( $1 \leq j \leq m$ ) are all derivable. Var applied to the first gives $Γ_{0}, x : A ⊢ x : A$ , and $m$ successive applications of Wk (with empty telescope), the $j$ -th using the $B_{j}$ judgment, extend the context one declaration at a time until $Γ ⊢ x : A$ is reached. Formally, induction on $m$ uses the displayed derivation as its base case; the successor case is one Wk whose type-formation premise is the next judgment extracted from context well-formedness. ◻

Exercise 26.13 ¶

★★☆ Write out the induction on $m$ in the proof of lemma 26.34, verifying the compressed premises of each Wk step against convention 26.14.

Referenced from 3 locations

Substitution as a rule and as an operation

Our rules perform substitution and weakening in one step. Both can instead be reconstructed by induction on derivations. That reconstruction is valid only when every added rule behaves uniformly under changes of context. We state this hypothesis exactly before beginning the proof.

Definition 26.35 — Economical presentation ¶

The economical presentation of a type theory over the structural core consists of the rules Ctx-Emp, Ctx-Ext, the equivalence rules of definition 26.16, the rules Assum, Conv, and Conv-Eq of lemma 26.34, lemma 26.31, lemma 26.32, taken as primitive, and the added rules of the theory stated with full premises. The presupposition, context-conversion, substitution, weakening, and Var rules are omitted.

Referenced from 3 locations

Definition 26.36 — Structurally stable rule schemes ¶

The structural stability of an added rule scheme is the conjunction of the following conditions; a scheme satisfying them is structurally stable.

It does not conclude a context judgment. Its full premises contain the context judgment and every direct presupposition of its conclusion, together with the formation or typing judgments for every expression parameter occurring in the conclusion.
Its ambient contexts are schematic. If one simultaneously inserts a fresh well-formed declaration at the same position in the ambient context of every premise and the conclusion, the result is another instance. The same is true when one simultaneously substitutes an element for an ambient variable, or replaces an ambient declaration by a judgmentally equal one. Local binder names are first freshened away from the inserted or substituted expressions. Repeating the insertion clause gives the same closure for an arbitrary well-formed telescope.
The expression parameters form a classified telescope, possibly with local binders. A type parameter $p_{i}$ has a formation judgment $Γ_{i} ⊢ p_{i} type$ ; a term parameter has a typing judgment $Γ_{i} ⊢ p_{i} : P_{i}$ . The context $Γ_{i}$ , and in the term case $P_{i}$ , may depend on earlier parameters. The phrase pointwise equal means, respectively, $p_{i} \equiv p_{i}^{'} type$ or $p_{i} \equiv p_{i}^{'} : P_{i}$ , after the primed classifier and every local context in $Γ_{i}$ have been transported along the equalities already obtained for earlier parameters. Every type-formation conclusion $F (\vec{p}) type$ has the congruence rule concluding $F (\vec{p}) \equiv F ({\vec{p}}^{'}) type$ from this telescope of equalities. Every term-typing conclusion $f (\vec{p}) : F (\vec{p})$ has a term-congruence rule at the unprimed result type; the primed result is first converted along the type congruence.
Every premise and conclusion is well scoped: all of its free variables are declared in its displayed context. The scheme is equivariant under fresh renaming of ambient and local variables; in particular, it contains no distinguished free object variable.

These are syntactic closure conditions on rule instances. In particular, a nullary axiom allowed only in the empty context is not structurally stable: it fails condition 2. Indeed, for a fixed closed $C$ the scheme $\frac{}{\cdot ⊢ c : C} closed - c$ has no inserted-context instance $x : A ⊢ c : C$ . A weakening induction whose last rule is closed- $c$ therefore stops: the induction hypotheses are empty, and condition 2 has no rule instance concluding $x : A ⊢ c : C$ . This is the minimal failure test for structural stability.

Referenced from 11 locations

Example 26.37 — A stable binding scheme ¶

Add an operator $Q$ of arity $(0, 1)$ and the formation scheme

Γ ⊢ C type

Γ, y : C ⊢ D type

Γ ⊢ Q (C; y . D) type

Q-form

Its full instance also contains $Γ ctx$ . Inserting $x : A$ in the ambient context produces the legal instance

Γ, x : A ⊢ C type

Γ, x : A, y : C ⊢ D type

Γ, x : A ⊢ Q (C; y . D) type

Q-form

If instead $Γ ⊢ a : E$ is substituted into an instance over $Γ, z : E$ , choose $y$ away from $a$ by equivariance. The resulting instance is

Γ ⊢ C [a / z] type

Γ, y : C [a / z] ⊢ D [a / z] type

Γ ⊢ Q (C [a / z]; y . D [a / z]) type

Q-form

Finally, its dependent congruence rule is

Γ ⊢ C \equiv C^{'} type

Γ, y : C ⊢ D \equiv D^{'} type

Γ, y : C^{'} ⊢ D^{'} type

Γ ⊢ Q (C; y . D) \equiv Q (C^{'}; y . D^{'}) type

Q-form-eq

The third premise forms the primed body in its own context. The second places that body in the unprimed context and compares the two bodies there, exactly the transport required by condition 3. This is the local-binder case of conditions 2 and 3.

Referenced from 2 locations

The Rules of Dependent Type Theory

Exercise 26.14 ¶

★★☆ Give $Q$ a term constructor $q (C; y . d) : Q (C; y . D)$ whose parameter $d$ has type $D$ in $Γ, y : C$ . Write its full typing scheme, its term-congruence scheme at the unprimed $Q$ -type, and the instance obtained from a rule over $Γ, z : E$ by substituting a given $Γ ⊢ a : E$ for $z$ .

Referenced from 3 locations

Regularity and arbitrary-telescope weakening are proved mutually because the regularity case for Assum needs weakening in a different telescope. Substitution transforms a derivation and its telescope simultaneously; context conversion then compares the transformed contexts. Equal substitution combines these facts with the classified congruence condition.

Lemma 26.38 — Regularity and weakening ¶

In an economical presentation with structurally stable added schemes, the following three assertions hold.

Every direct presupposition rule is admissible.
If $Γ, Θ ctx$ and $Γ, Δ ⊢ J$ , then $Γ, Θ, Δ ⊢ J$ is derivable whenever the displayed context pieces have pairwise disjoint domains.
Under the same context hypotheses, a derivation of $Γ, Δ ctx$ is transformed into one of $Γ, Θ, Δ ctx$ .

The one-declaration case of clause 2 is Wk.

Referenced from 5 locations

The Rules of Dependent Type Theory

Proof of Lemma 26.38 — Regularity and weakening

Proof. For each height $h$ , prove simultaneously: (i) every direct presupposition of the conclusion of a derivation of height at most $h$ ; (ii) for every split $Γ, Δ$ of its context and every telescope $Θ$ satisfying the displayed hypotheses, the judgment-weakening transformation of clause 2; and (iii) the corresponding context transformation of clause 3. Thus $Θ$ is universally quantified inside the induction hypothesis. The whole well-formed telescope $Θ$ is fixed during one recursive transformation; it is not inserted by repeated appeals to the induction hypothesis. The regularity assertion produces every direct presupposition of the conclusion.

For a context derivation, keep the insertion point between $Γ$ and $Δ$ . If $Δ$ is empty, the target is the fixed derivation of $Γ, Θ ctx$ . If the final Ctx-Ext introduces a declaration in $Δ$ , apply the judgment-weakening induction hypothesis to its sole type premise, inserting the entire $Θ$ , and reapply Ctx-Ext. The regularity induction hypothesis for that same premise gives the transformed prefix context when required. The type premise is also the direct presupposition of the resulting context.

For Assum, weakening the conclusion only enlarges its well-formed context; the same declaration is still present, so Assum applies again. For regularity, write the context as $Γ_{0}, y : B, Γ_{1}$ , where the selected declaration is $y : B$ . A context derivation in the economical system ends in iterated Ctx-Ext; its subtree at this declaration contains $Γ_{0} ⊢ B type$ . This subtree has smaller height. Apply the telescope-weakening induction hypothesis once, with telescope $y : B, Γ_{1}$ , to obtain $Γ_{0}, y : B, Γ_{1} ⊢ B type$ , the presupposition of the Assum conclusion. This is the case that forces regularity and weakening to be simultaneous.

For an equivalence rule, Conv, or Conv-Eq, transform all premises and reapply the same rule. Their presuppositions follow from the transformed typing premises, using symmetry where the right side of an equality is required. For an added scheme, condition 2 of definition 26.36 makes the weakened premises another legal instance, and condition 1 gives the direct presuppositions. Condition 4 permits an equivariant choice of local names disjoint from the inserted telescope. These are all final rules. Taking $Θ = x : A$ gives Wk. ◻

Lemma 26.39 — Ordinary substitution in the economical presentation ¶

In an economical presentation with structurally stable added schemes, suppose $Γ ⊢ a : A$ is derivable economically. Then ordinary substitution has both of the following simultaneous clauses:

if $Γ, x : A, Δ ctx$ , then $Γ, Δ [a / x] ctx$ ;
if $Γ, x : A, Δ ⊢ J$ for any of the four judgment theses, then $Γ, Δ [a / x] ⊢ J [a / x]$ .

Referenced from 3 locations

The Rules of Dependent Type Theory

Proof of Lemma 26.39 — Ordinary substitution in the economical presentation

Proof. Induct on the second derivation, simultaneously for contexts and all four theses. In a context derivation, a final Ctx-Ext whose declaration lies in $Δ$ is rebuilt from its transformed type premise. If it is the distinguished declaration $x : A$ itself, then $Δ$ is empty: substitution deletes that final Ctx-Ext, leaving $Γ ctx$ , a presupposition of the fixed derivation of $a$ . The equivalence rules, Conv, and Conv-Eq are obtained by transforming their premises and reapplying the same rule. An added scheme is handled in the same way by condition 2 of definition 26.36.

Only Assum requires a calculation. If its selected variable is $x$ , use the fixed derivation of $a$ and weaken it along $Δ [a / x]$ by lemma 26.38. If the variable is declared in $Γ$ , apply Assum there and weaken along the substituted telescope. If it is declared in $Δ$ , its declaration in the new context is precisely the old one with $a$ substituted, so Assum applies directly. These three cases give exactly $Γ, Δ [a / x] ⊢ J [a / x] .$ A simultaneous rule induction gives the scoping invariant $FV (a) \subseteq dom (Γ)$ : check the economical structural rules directly and use condition 4 for an added rule. Since raw context concatenation makes $dom (Γ)$ and $dom (Δ)$ disjoint, every declared name of $Δ$ already avoids $FV (a)$ . Thus the displayed context substitution is defined; no context variable has been renamed. ◻

Lemma 26.40 — Context conversion in the economical presentation ¶

In an economical presentation with structurally stable added schemes, if $Γ ⊢ A \equiv A^{'} type$ and $Γ, x : A, Δ ⊢ J$ are derivable economically, then so is $Γ, x : A^{'}, Δ ⊢ J$ . Simultaneously, a derivation of $Γ, x : A, Δ ctx$ is transformed into one of $Γ, x : A^{'}, Δ ctx$ .

Referenced from 5 locations

Proof of Lemma 26.40 — Context conversion in the economical presentation

Proof. Induct simultaneously on context and judgment derivations, keeping the distinguished declaration marked. In a context derivation, a final Ctx-Ext to the left of $x : A$ is retained. To the right, transform both the prefix context recovered from its type premise and the type premise itself before reapplying Ctx-Ext. At the distinguished declaration itself, use the right-hand type presupposition of $A \equiv A^{'}$ and Ctx-Ext to form $Γ, x : A^{'}$ . Transform the premises of every other nonvariable rule and reapply that rule; condition 2 of definition 26.36 gives the added-scheme instances. For Assum, variables declared in $Γ$ or $Δ$ are reintroduced by the same rule. For the distinguished variable, Assum gives $x : A^{'}$ in $Γ, x : A^{'}$ . Weaken the symmetric equality $A^{'} \equiv A$ to that context and apply primitive Conv; then weaken along $Δ$ . Thus the transformed variable has the original type $A$ , as the unchanged thesis requires. This completes every final-rule case. ◻

If $A \equiv A^{'}$ , we may therefore carry any telescope declared after $x : A$ over to the context declaring $x : A^{'}$ .

Lemma 26.41 — Equal substitution in the economical presentation ¶

In an economical presentation with structurally stable added schemes, let $Γ ⊢ a \equiv a^{'} : A$ . Economical derivations of $Γ, x : A, Δ ⊢ B type$ and $Γ, x : A, Δ ⊢ b : B$ can be transformed respectively into $Γ, Δ [a / x] ⊢ B [a / x] \equiv B [a^{'} / x] type,$ and $Γ, Δ [a / x] ⊢ b [a / x] \equiv b [a^{'} / x] : B [a / x] .$

Referenced from 3 locations

The Rules of Dependent Type Theory

Proof of Lemma 26.41 — Equal substitution in the economical presentation

Proof. First form a finite presupposition-expanded derivation. At every node attach, as subsidiary trees, derivations of all direct presuppositions established by lemma 26.38; recursively attach the presuppositions of a nonempty context by peeling its last declaration. The regularity construction uses only proper premise subderivations (in the Assum case, a proper context subtree), while context peeling strictly shortens the context. Hence the expansion is finite and well founded. We induct on the height of this expanded tree, counting the attached subsidiary trees; every premise or presupposition invoked below is then a proper subtree. The telescope $Δ$ is arbitrary and is not part of the measure.

Write $Δ = y_{1} : B_{1}, \dots, y_{m} : B_{m}$ , and write $Δ_{i - 1}$ for its first $i - 1$ declarations. Simultaneously maintain a third assertion for a context derivation of $Γ, x : A, Δ$ : for every declaration $y_{i} : B_{i}$ it constructs $\begin{matrix} (*) & Γ, Δ_{i - 1} [a / x] ⊢ B_{i} [a / x] \equiv B_{i} [a^{'} / x] type . \end{matrix}$ Before the marked declaration, and at Ctx-Emp, the assertion is empty. At the Ctx-Ext that introduces $x : A$ , substitution removes that declaration and still introduces no clause of $(*)$ . At a later Ctx-Ext, the context and type premises have smaller height. The context induction hypothesis treats the earlier declarations, and the type induction hypothesis gives the next instance of $(*)$ . Repeated use of lemma 26.40, with the symmetric orientation of each equality in $(*)$ , therefore transports every right-hand substituted premise from $Δ [a^{'} / x]$ to the common context $Δ [a / x]$ . This explains the common context in both conclusions.

Now inspect a type-formation or term-typing derivation. In the Assum case, ordinary substitution applied to the attached context presupposition $Γ, x : A, Δ ctx$ gives $Γ, Δ [a / x] ctx$ . If the selected variable is $x$ , the fixed equality $a \equiv a^{'} : A$ is weakened along $Δ [a / x]$ . Any other selected variable is reintroduced in this common context by Assum, and Tm-Refl gives the required equality directly; no conversion through $Δ [a^{'} / x]$ is needed. In the Conv case, the induction hypothesis first gives equality of the two substituted terms at the old type. Ordinary substitution of the type-equality premise gives the converted type equality, and primitive Conv-Eq moves the term equality to that type.

For an added formation or typing rule, apply the induction hypotheses to the full typing premises of all expression parameters. Condition 3 of definition 26.36 then gives the displayed type or term equality. Equality premises of the rule are substituted ordinarily on each side; no “equality between equality derivations” is required. A premise under an additional local binder still has smaller derivation height, so the induction hypothesis applies with that binder appended to the arbitrary telescope. For example, a premise $Γ, x : A, Δ, y : C ⊢ D type$ produces $Γ, Δ [a / x], y : C [a / x] ⊢ D [a / x] \equiv D [a^{'} / x] type,$ after the induction hypothesis for the parameter premise has given $C [a / x] \equiv C [a^{'} / x]$ . This is the binding case that a length-first induction would miss. All recursive calls are to proper premise subderivations, so height induction is well founded. ◻

Equal substitution is the last missing structural operation; all four derivation transformations can now be assembled.

Corollary 26.42 — Simultaneous structural admissibility ¶

In an economical presentation with structurally stable added schemes, the presupposition, weakening, substitution, context-conversion, and equal-substitution rules are admissible.

Referenced from 3 locations

The Rules of Dependent Type Theory

Proof of Corollary 26.42 — Simultaneous structural admissibility

Proof. Combine lemma 26.38, lemma 26.39, lemma 26.40, lemma 26.41. ◻

Theorem 26.43 — Equivalence of presentations ¶

Let $T$ be the structural rules of definition 26.22 extended by structurally stable rule schemes in the sense of definition 26.36, and let $T^{-}$ be its economical presentation. Then a judgment is derivable in $T$ if and only if it is derivable in $T^{-}$ . In particular, Subst, Wk, Ctx-Conv, and the presupposition rules are admissible in $T^{-}$ .

Referenced from 7 locations

Proof of Theorem 26.43 — Equivalence of presentations

Proof. ( $T^{-} \subseteq T$ .) Every primitive rule of $T^{-}$ is derivable in $T$ : Assum, Conv, and Conv-Eq by lemma 26.34, lemma 26.31, lemma 26.32; every other primitive rule is shared. Replace each use of a derived primitive by its displayed derivation. Rule induction translates the whole tree.

( $T \subseteq T^{-}$ .) By corollary 26.42, every omitted structural rule has a derivation transformation in $T^{-}$ . Translate a $T$ -derivation by rule induction: retain a shared rule and replace each omitted structural rule by the corresponding admissibility transformation. In the Var case, the transformed premise $Γ ⊢ A type$ first gives $Γ, x : A ctx$ by Ctx-Ext; primitive Assum then gives $Γ, x : A ⊢ x : A$ . The transformed premises have already been obtained by the induction hypotheses, so the result is a $T^{-}$ -derivation of the same judgment. ◻

The structural-admissibility argument above follows the formulation surveyed by Hofmann [Hof97].

Remark 71.47 ¶

Equivalence of structural presentations is not a type-checking algorithm. For each added former a kernel still needs formation and typing generation lemmas, injectivity of type constructors, a terminating and complete conversion procedure (usually obtained from confluence and normalization), and bidirectional rules that expose the input/output modes. The concrete interface must, for example, recover the domain and codomain of a function type from its head constructor, and conversion must decide whether an inferred type agrees with an expected type. This is why a displayed declarative rule set, although complete as a specification, is not yet executable.

Exercise 26.15 ¶

★★☆ Verify the direction $T^{-} \subseteq T$ of theorem 26.43 in detail: exhibit each primitive rule of $T^{-}$ as a derivable rule of $T$ , and explain why derivability suffices to translate whole derivations.

Referenced from 3 locations

Remark 26.44 ¶

In $T^{-}$ the rules Subst and Wk are admissible but are not primitive. The construction in theorem 26.43 is a recursive transformation of an input derivation. Its final-rule case uses exactly the stability interface of definition 26.36; the closed-only axiom above shows the transformation getting stuck when that interface is absent.

Referenced from 2 locations

The Rules of Dependent Type Theory

Substitution by a whole context

One Subst step removes one declaration. Eliminators for pair-like data must often replace an entire dependent telescope, so we package the elements needed for all declarations and then substitute them in order.

Definition 26.45 — Context substitution ¶

Let $Γ, Δ ctx$ , where $Δ = y_{1} : B_{1}, \dots, y_{m} : B_{m}$ is a telescope over $Γ$ . A context substitution $f : Γ \Rightarrow Δ$ is a list $(b_{1}, \dots, b_{m})$ such that no $y_{i}$ is free in any $b_{j}$ and $Γ ⊢ b_{j} : B_{j} [b_{1} / y_{1}, \dots, b_{j - 1} / y_{j - 1}] (1 \leq j \leq m) .$

Referenced from 8 locations

For example, if $Γ, x : A, y : B ctx$ , $Γ ⊢ a : A$ , and $Γ ⊢ b : B [a / x]$ , then $(a, b) : Γ \Rightarrow (x : A, y : B)$ . This is the two-declaration substitution used by dependent pair elimination.

Proposition 26.46 — Substitution by a context ¶

If $f : Γ \Rightarrow Δ$ and $Γ, Δ ⊢ J$ , then $Γ ⊢ J [b_{1} / y_{1}, \dots, b_{m} / y_{m}] .$

Referenced from 5 locations

Proof of Proposition 26.46 — Substitution by a context

Proof. Substitute $b_{1}$ for $y_{1}$ . The next declaration becomes $y_{2} : B_{2} [b_{1} / y_{1}]$ , exactly the type of $b_{2}$ in definition 26.45; hence the next Subst applies. Continuing in order removes all $m$ declarations and gives the iterated substitution displayed in the conclusion. Because no inserted $b_{j}$ contains a target variable $y_{i}$ , a structural induction on $J$ identifies this iteration with the one-pass simultaneous substitution of definition 26.10. ◻

The preceding proposition is the null-source case of a more useful relative construction. Suppose that both $Γ, Θ$ and $Γ, Δ$ are contexts, where $Δ = y_{1} : B_{1}, \dots, y_{m} : B_{m}$ . A relative telescope map $f : Θ \Rightarrow_{Γ} Δ$ is a list $(b_{1}, \dots, b_{m})$ satisfying $Γ, Θ ⊢ b_{j} : B_{j} [b_{1} / y_{1}, \dots, b_{j - 1} / y_{j - 1}] (1 \leq j \leq m),$ where the displayed brackets denote one-pass simultaneous substitution. Source and target telescopes are understood up to alpha-equivalence: before composing distinct maps, choose their nonshared binders disjoint. No freshness condition is imposed on the entries. In particular, when the source is the target, an entry may be the corresponding target variable. Thus $f : Γ \Rightarrow Δ$ in definition 26.45 is the case $Θ = ()$ .

Proposition 71.51 — Identity and composition of telescope maps ¶

Relative telescope maps have the following operations.

The variable list $(y_{1}, \dots, y_{m})$ is an identity map ${id}_{Δ} : Δ \Rightarrow_{Γ} Δ$ .
If $f : Θ \Rightarrow_{Γ} Δ$ has entries $b_{i}$ and $g : Ξ \Rightarrow_{Γ} Θ$ has entries $c_{k}$ , then $f \circ g : = (b_{1} [g], \dots, b_{m} [g]) : Ξ \Rightarrow_{Γ} Δ,$ where $b_{i} [g]$ is simultaneous substitution of the $c_{k}$ for the variables of $Θ$ .
If $Γ, Δ ⊢ J$ , then $f$ acts on the judgment by one-pass simultaneous substitution of the entries of $f$ for the variables of $Δ$ . The result is derivable over $Γ, Θ$ , and the action satisfies $J [{id}_{Δ}] = J, (J [f]) [g] = J [f \circ g] .$ Consequently composition is associative and the displayed identities are left and right units, up to alpha-equivalence of raw expressions.

Referenced from 8 locations

Proof of Proposition 71.51 — Identity and composition of telescope maps

Proof. First choose a representative whose binders avoid every source and target variable and every free variable in the entries of $f$ and $g$ . Structural induction on that representative proves $E [{id}_{Δ}] = E, (E [f]) [g] = E [f \circ g]$ for every raw expression $E$ . At a target variable the second equation is the definition $b_{i} [g] = (f \circ g)_{i}$ ; at any other variable both sides leave the variable fixed or apply the same entry of $g$ . An operator case applies the induction hypotheses to all bodies and restores its binder lists. The synchronized-display argument of proposition 26.11.1 makes the calculation independent of the chosen representative.

For the identity, repeated use of Assum gives each $y_{j}$ at the type required by the relative-map definition: substituting each earlier variable for itself fixes $B_{j}$ . For composition, apply substitution by the whole telescope $g$ to the typing judgment for each $b_{j}$ . The notation $(f \circ g)_{< j} / y_{< j}$ abbreviates substitution of the first $j - 1$ components of $f \circ g$ for $y_{1}, \dots, y_{j - 1}$ . The resulting type is $B_{j} [(f \circ g)_{< j} / y_{< j}],$ by the raw composition equation just proved. These are exactly the premises required for $f \circ g$ to be a relative telescope map.

For the action on judgments, choose a fresh alpha-copy $\hat{Δ}$ of $Δ$ , disjoint from $Γ, Θ$ and from every entry of $f$ , and rename $Γ, Δ ⊢ J$ to $Γ, \hat{Δ} ⊢ \hat{J}$ . General weakening now gives $Γ, Θ, \hat{Δ} ⊢ \hat{J}$ . Substitute the entries of $f$ for the fresh variables of $\hat{Δ}$ in telescope order. Their typing premises are exactly the renamed telescope types after the preceding substitutions, so repeated Subst yields $Γ, Θ ⊢ \hat{J} [f]$ ; by construction this is the one-pass action $J [f]$ . A second choice of fresh copy gives an alpha-equivalent derivation.

The two displayed action laws are the raw identity and composition equations proved above. Applying the composition equation twice gives $(f \circ g) \circ h = f \circ (g \circ h)$ componentwise; applying the identity clause gives both unit laws. Alpha-equivalence accounts only for the fresh names chosen under binders. ◻

Exercise 26.16 ¶

★☆☆ For the two-declaration context substitution $(a, b)$ above, write the two successive instances of Subst that transform $Γ, x : A, y : B ⊢ J$ into $Γ ⊢ J [a / x, b / y]$ . Indicate where the premise $Γ ⊢ b : B [a / x]$ is used.

Referenced from 3 locations

If $Δ$ is a standalone context and $Δ ⊢ J$ , the standalone form of context substitution follows from proposition 26.46: weaken the context and the judgment by the declarations of $Γ$ in order, obtaining the relative source $Γ, Δ ⊢ J$ , and then apply the proposition.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 71.17, then complete exercise 71.20.

Exercise 71.17 ¶

★★☆ Reconstruct the Assum case of the induction proving general weakening. Suppose the final judgment $Γ, Δ ⊢ z : C$ ends in Assum, and a fresh declaration $x : A$ is inserted immediately after $Γ$ . Separate the case in which the declaration $z : C$ lies in $Γ$ from the case in which $Δ = Δ_{1}, z : C, Δ_{2}$ . In each case, identify the context-formation premise that lets Assum be replayed in the enlarged context.

Referenced from 4 locations

Exercise 71.18 ¶

★★☆ Let $Δ = (x : A, y : B (x))$ , $Θ = (u : C, v : D (u))$ , and $Ξ = (w : E)$ be telescopes over the same base $Γ$ . For $f = (b_{1}, b_{2}) : Θ \Rightarrow_{Γ} Δ$ and $g = (c_{1}, c_{2}) : Ξ \Rightarrow_{Γ} Θ$ , write $f \circ g$ componentwise. Derive the type of its second component from Subst. For a further map $h : Ω \Rightarrow_{Γ} Ξ$ , prove associativity by comparing both composites with one-pass capture-avoiding substitution.

Referenced from 3 locations

Exercise 71.19 ¶

★★☆ Consider the tempting definition of a relative telescope map which requires every target variable to be fresh for every component. Apply it to the identity map on $Δ = (u : A, v : B (u))$ . Give the first component at which the definition fails, and explain why alpha-renaming the target before acting on a judgment repairs the proof without imposing this false side condition on the map itself.

Referenced from 3 locations

Exercise 71.20 ¶

★★★ Practical project.dtt-substitution-auditor Implement named-variable capture-avoiding substitution in Agda or Kappa, together with a checker for the local scoping invariant $FV (t [u / x]) \subseteq (FV (t) ∖ {x}) \cup FV (u),$ where the implementation first alpha-renames binders to avoid capture. Test the binder inputs $L (y . x) [y / x]$ , $L (y . P (x; y)) [z / x]$ , and a two-declaration context substitution; the first output must be alpha-equivalent to $L (y^{'} . y)$ and every output must pass the scoping checker. Before implementing the checker, perform these three substitutions on paper and mark the binder renaming that prevents capture. These calculations are the finite specification against which the implementation is tested.

Referenced from 5 locations

Sources. The judgment forms originate with Martin-Löf [ML98, ML84]. Abstract binding trees are developed by Harper [Har16], and the structural-admissibility and context-substitution arguments are treated by Hofmann [Hof97]. The citations record provenance and provide alternative formulations.