Chapter 72Core route

Dependent Products, Sums, and Unit

The structural rules can substitute an element into a family, but they cannot yet package a family of elements into one object. Suppose $Γ, x : A ⊢ B type and Γ, x : A ⊢ b : B .$ We want a type whose elements are such dependent assignments $x \mapsto b$ , and a second type whose elements contain $a : A$ together with $b : B [a / x]$ . Dependent products and sums provide these two objects. A one-element type serves when no data is to be packaged.

Dependent products

The dependent product $\prod_{x : A} B$ is the type of dependent functions: an element assigns to every $a : A$ an element of the instance $B [a / x]$ .

Extend the raw syntax of definition 26.1 by $\prod_{x : A} B$ , $λ (x : A) . b$ , and $f a$ . The product former and dependent abstraction have arity $(0, 1)$ and bind $x$ in their second argument; application has arity $(0, 0)$ . The domain $A$ in $λ (x : A) . b$ is a raw argument, so changing it changes the raw term. Alpha-equivalence and capture-avoiding substitution for these expressions are therefore the operations already defined in convention 26.8, definition 26.10.

Convention 27.1 — Formation, introduction, elimination, computation ¶

A type former is specified by displayed rules in the following fixed order:

formation: how the new type is formed from given data;
introduction: how elements of the new type are constructed;
elimination: how elements of the new type are used;
computation: the $β$ -rules, stating how elimination acts on introduced elements, followed — when present — by a uniqueness ( $η$ -) rule, stating that every element is determined by its behavior under elimination.

Each rule presupposes the formation judgments needed to type its premises, as specified by convention 26.14. Every constructor is congruent in its arguments; when an argument is dependent, the congruence rule includes the required context and type conversions. The dependent instances below make these conversions explicit.

Referenced from 14 locations

A $β$ -rule evaluates an elimination applied to an introduction. An $η$ -rule applies where no $β$ -rule can: it rebuilds an arbitrary element from its observable parts. The calculations after each rule display show both roles.

Definition 27.2 — Rules for Π ¶

The dependent-product former is given by the following rules, in the order of convention 27.1.

Γ, x : A ⊢ B type

Γ ⊢ \prod_{x : A} B type

Π-form

Γ, x : A ⊢ b : B

Γ ⊢ λ (x : A) . b : \prod_{x : A} B

Π-intro

Γ ⊢ f : \prod_{x : A} B

Γ ⊢ a : A

Γ ⊢ f a : B [a / x]

Π-elim

Γ, x : A ⊢ b : B

Γ ⊢ a : A

Γ ⊢ (λ (x : A) . b) a \equiv b [a / x] : B [a / x]

Π-β

Γ ⊢ f : \prod_{x : A} B

Γ ⊢ f \equiv λ (x : A) . f x : \prod_{x : A} B

Π-η

In $Π$ -form and $Π$ -intro the variable $x$ becomes bound in $B$ and in $b$ . In $Π$ - $η$ , choose the displayed binder $x$ to occur nowhere in $f$ ; this is possible by lemma 26.9. The premise $Γ ⊢ A type$ is presupposed throughout (convention 26.14).

Referenced from 26 locations

Here are the two basic calculations. If $Γ, x : A ⊢ b : B$ and $Γ ⊢ a : A$ , then $Γ ⊢ λ (x : A) . b : \prod_{x : A} B, (λ (x : A) . b) a \equiv b [a / x] : B [a / x] .$ The first expression introduces a dependent function; the second applies it and computes by $β$ . Conversely, if $Γ ⊢ f : \prod_{x : A} B$ , then $f \equiv λ (x : A) . f x : \prod_{x : A} B .$ This is $η$ : even when $f$ is a variable and no $β$ -step is possible, its values determine it judgmentally.

Remark 27.3 — Notation ¶

Family instances retain their binding information: if $Γ, x : A ⊢ B type$ , the instance at $a$ is always $B [a / x]$ . Functions of several arguments are iterated products $\prod_{x : A} \prod_{y : B} C$ , abbreviated $\prod_{x, y : A} C$ when both binders range over the same type; iterated application is $f a b$ . Application associates to the left and binds more tightly than $λ$ -abstraction.

Referenced from 2 locations

Dependent Products, Sums, and Unit

Remark 27.4 — The congruence pattern ¶

Each operator of definition 27.2 has a congruence rule. For the type former, abstraction, and application they read:

Γ ⊢ A \equiv A^{'} type

Γ, x : A ⊢ B \equiv B^{'} type

Γ ⊢ \prod_{x : A} B \equiv \prod_{x : A^{'}} B^{'} type

Π-form-eq

Γ ⊢ A \equiv A^{'} type

Γ, x : A ⊢ B \equiv B^{'} type

Γ, x : A ⊢ b \equiv b^{'} : B

Γ ⊢ λ (x : A) . b \equiv λ (x : A^{'}) . b^{'} : \prod_{x : A} B

λ-eq

Γ ⊢ f \equiv f^{'} : \prod_{x : A} B

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

Γ ⊢ f a \equiv f^{'} a^{'} : B [a / x]

app-eq

In $Π$ -form-eq, context conversion first types $B^{'}$ in $Γ, x : A^{'}$ . For $λ$ -eq, context and type conversion give $\begin{aligned} Γ, x : A^{'} ⊢ b^{'} : B^{'}, \\ Γ ⊢ λ (x : A^{'}) . b^{'} : \prod_{x : A^{'}} B^{'}, \\ \prod_{x : A^{'}} B^{'} \overset{symmetry of Π -form-eq}{\equiv} \prod_{x : A} B . \end{aligned}$ Rule Conv therefore places the right abstraction in the conclusion’s type. For application, equal substitution and conversion give the local chain $f^{'} a^{'} : B [a^{'} / x], B [a^{'} / x] \overset{S u b s t - E q - T y}{\equiv} B [a / x], f^{'} a^{'} : B [a / x] by Conv .$ Thus every conclusion compares terms in one context and one type.

Referenced from 6 locations

Exercise 27.1 ¶

★★☆ In chapter 2 the clause $A, B \mapsto A \to B$ belongs to the grammar of simple types, while abstraction and application are typing rules. Place these three clauses in the formation, introduction, and elimination positions of convention 27.1. Add the usual $β$ - and $η$ -equations as a hypothetical fourth group, noting that chapter 2 itself has no judgmental equality and that $λ x . f x = f$ requires $x \notin FV (f)$ . Compare the result with definition 27.2: which codomains and premises acquire a dependence on the argument?

Referenced from 3 locations

Definition 27.5 — Ordinary functions ¶

Let $Γ ⊢ A type$ and $Γ ⊢ B type$ . Weakening $B$ by $A$ (definition 26.21) and applying $Π$ -form forms a constant dependent product. Choose $x \notin dom (Γ)$ occurring nowhere in $B$ , and define the function type by $A \to B : = \prod_{x : A} B .$ This notation associates to the right. The identity function is ${id}_{A} : = λ (x : A) . x : A \to A .$ For $Γ ⊢ f : A \to B$ and $Γ ⊢ g : B \to C$ , define $g \circ f : = λ (x : A) . g (f x) : A \to C .$

Referenced from 2 locations

Dependent Products, Sums, and Unit

Example 27.6 — The generic evaluation ¶

Let $Γ ⊢ A type$ and $Γ, x : A ⊢ B type$ . Form the context $Γ, f : \prod_{x : A} B, a : A .$ The last occurrence of $A$ is obtained by weakening it past $f$ . Context formation and the general variable rule lemma 26.34 give $f : \prod_{x : A} B$ and $a : A$ in this context; $Π$ -elim then gives the genuinely dependent evaluation $f a : B [a / x]$ .

Γ, f : \prod_{x : A} B, a : A ctx

(f : \prod_{x : A} B) \in (Γ, f : \prod_{x : A} B, a : A)

Γ, f : \prod_{x : A} B, a : A ⊢ f : \prod_{x : A} B

Assum

Γ, f : \prod_{x : A} B, a : A ctx

(a : A) \in (Γ, f : \prod_{x : A} B, a : A)

Γ, f : \prod_{x : A} B, a : A ⊢ a : A

Assum

Γ, f : \prod_{x : A} B, a : A ⊢ f a : B [a / x]

Π-elim

If $f$ is a variable, this application is neutral: no $β$ -rule applies. The $η$ -rule nevertheless gives $f \equiv λ (x : A) . f x$ .

Referenced from 3 locations

Dependent Products, Sums, and Unit

Lemma 27.7 — Category laws ¶

Let $Γ ⊢ f : A \to B$ , $Γ ⊢ g : B \to C$ , and $Γ ⊢ h : C \to D$ . Then $\begin{aligned} Γ & ⊢ (h \circ g) \circ f \equiv h \circ (g \circ f) : A \to D, \\ Γ & ⊢ {id}_{B} \circ f \equiv f : A \to B, Γ ⊢ f \circ {id}_{A} \equiv f : A \to B . \end{aligned}$

Referenced from 5 locations

Dependent Products, Sums, and Unit

Proof of Lemma 27.7 — Category laws

Proof. Associativity. Rule $Π$ - $β$ for the abstraction $h \circ g$ gives $(h \circ g) (f x) \equiv h (g (f x))$ in context $Γ, x : A$ , so $(h \circ g) \circ f \overset{d e f i n i t i o n 27.5}{=} λ (x : A) . (h \circ g) (f x) \overset{λ - e q}{\equiv} λ (x : A) . h (g (f x)) .$ Expanding the outer composite on the other side gives $\begin{aligned} h \circ (g \circ f) & \overset{d e f i n i t i o n 27.5}{=} λ (x : A) . h ((g \circ f) x) \\ \overset{Π - β, a p p - e q, λ - e q}{\equiv} λ (x : A) . h (g (f x)) . \end{aligned}$ Let $n : = λ (x : A) . h (g (f x))$ . The first chain derives $((h \circ g) \circ f) \equiv n$ , and the second derives $(h \circ (g \circ f)) \equiv n$ . Apply symmetry to the second derivation to obtain $n \equiv h \circ (g \circ f)$ , then compose the two derivations by transitivity (definition 26.16).

Left unit: ${id}_{B} \circ f \overset{d e f i n i t i o n 27.5}{=} λ (x : A) . {id}_{B} (f x) \overset{Π - β, λ - e q}{\equiv} λ (x : A) . f x \overset{Π - η}{\equiv} f .$ Right unit: $f \circ {id}_{A} \overset{d e f i n i t i o n 27.5}{=} λ (x : A) . f ({id}_{A} x) \overset{Π - β, a p p - e q, λ - e q}{\equiv} λ (x : A) . f x \overset{Π - η}{\equiv} f,$ using $Π$ - $β$ , app-eq, $λ$ -eq, and finally $Π$ - $η$ . Thus the unit laws, unlike associativity, genuinely use the $η$ -rule. ◻

Proposition 27.8 — Evaluation-style elimination ¶

In the presence of weakening, the variable rule, and substitution, $Π$ -elim is interderivable with the evaluation rule

Γ ⊢ f : \prod_{x : A} B

Γ, z : A ⊢ f z : B [z / x]

Π-ev

where $z$ is chosen fresh for $Γ, f, A, B$ .

Referenced from 3 locations

Dependent Products, Sums, and Unit

Proof of Proposition 27.8 — Evaluation-style elimination

Proof. Given $Π$ -elim, derive $Π$ -ev exactly as in example 27.6: weaken $f$ to $Γ, z : A$ , obtain $Γ, z : A ⊢ z : A$ by Var, and apply. Conversely, given $Π$ -ev and a term $Γ ⊢ a : A$ , the substitution rule of definition 26.20 applied to $Γ, z : A ⊢ f z : B [z / x]$ yields the required term at $B [a / x]$ . Since $z$ was chosen fresh for $f$ , the defining clauses of definition 26.10 give $(f z) [a / z] = f a$ . The corresponding translation of the computation rule substitutes $a$ for the fresh generic variable in the generic $β$ equation. Freshness gives $((λ (x : A) . b) z) [a / z] = (λ (x : A) . b) a$ , $b [z / x] [a / z] = b [a / x]$ , and $B [z / x] [a / z] = B [a / x]$ . Thus both terms have the required type $B [a / x]$ , so Subst-Eq-Tm yields the ordinary $Π$ - $β$ rule. ◻

Exercise 27.2 ¶

★★☆ ( $η$ as judgmental extensionality.) Show that, given the other rules of definition 27.2, the rule $Π$ - $η$ is equivalent to the extensionality rule: from $Γ ⊢ f : \prod_{x : A} B$ , $Γ ⊢ g : \prod_{x : A} B$ , and $Γ, x : A ⊢ f x \equiv g x : B$ , infer $Γ ⊢ f \equiv g : \prod_{x : A} B$ . (For the forward direction, rebuild $f$ and $g$ by $η$ ; for the converse, instantiate $g : = λ (x : A) . f x$ and compute with $Π$ - $β$ .)

Referenced from 3 locations

Exercise 27.3 ¶

★☆☆ Rewrite the right-unit calculation in lemma 27.7 as a derivation of $Γ ⊢ f \circ {id}_{A} \equiv f : A \to B$ , displaying the uses of application congruence, abstraction congruence, and $η$ .

Referenced from 3 locations

Exercise 27.4 ¶

★★☆ Complete proposition 27.8: show that in the presence of the structural rules, the rule $Π$ - $β$ is interderivable with its generic instance $Γ, x : A ⊢ (λ (y : A) . b [y / x]) x \equiv b : B$ , where $y$ occurs nowhere in $b, B, Γ, A$ and is distinct from $x$ . In the reverse direction substitute an arbitrary $Γ ⊢ a : A$ for $x$ and use the substitution-composition equation of proposition 26.11.

Referenced from 3 locations

Exercise 27.5 ¶

★☆☆ Let $Γ ⊢ A type$ , $Γ ⊢ B type$ , and $Γ ⊢ C type$ . In context $Γ, y : B$ , define ${const}_{y}^{A \to B} : = λ (x : A) . y : A \to B$ ; the superscript records the domain and codomain of the constant map. If $Γ ⊢ f : A \to B$ , prove in context $Γ, z : C$ that ${const}_{z}^{B \to C} \circ f \equiv {const}_{z}^{A \to C} : A \to C .$ If $Γ ⊢ g : B \to C$ , prove in context $Γ, y : B$ that $g \circ {const}_{y}^{A \to B} \equiv {const}_{g y}^{A \to C} : A \to C .$

Referenced from 3 locations

Exercise 27.6 ¶

★★☆ Let $Γ ⊢ A type$ , $Γ ⊢ B type$ , and $Γ, x : A, y : B ⊢ C type$ . Construct a term $σ : (\prod_{x : A} \prod_{y : B} C) \to (\prod_{y : B} \prod_{x : A} C)$ swapping the arguments, and show $σ^{'} \circ σ \equiv id$ , where $σ^{'}$ is the swap in the other direction. Begin with $λ (f : \prod_{x : A} \prod_{y : B} C) . λ (y : B) . λ (x : A) . f x y$ ; use lemma 26.33 to form $C$ in the swapped context, and use $η$ twice in the round trip.

Referenced from 3 locations

Dependent sums

The dependent sum $\sum_{x : A} B$ is the type of dependent pairs: an element consists of an $a : A$ together with an element of the instance $B [a / x]$ . We present $Σ$ negatively, with projections and an $η$ -rule.

Extend the raw syntax by $\sum_{x : A} B$ , $(a, b)$ , ${pr}_{1} (p)$ , and ${pr}_{2} (p)$ . The sum former has arity $(0, 1)$ and binds $x$ in its second argument; pairing has arity $(0, 0)$ and each projection has arity $(0)$ .

Definition 27.9 — Rules for Σ ¶

The dependent-sum former is given by the following rules; congruence rules are tacit (convention 27.1).

Γ, x : A ⊢ B type

Γ ⊢ \sum_{x : A} B type

Σ-form

Γ, x : A ⊢ B type

Γ ⊢ a : A

Γ ⊢ b : B [a / x]

Γ ⊢ (a, b) : \sum_{x : A} B

Σ-intro

Γ ⊢ p : \sum_{x : A} B

Γ ⊢ {pr}_{1} (p) : A

Σ-elim_1

Γ ⊢ p : \sum_{x : A} B

Γ ⊢ {pr}_{2} (p) : B [{pr}_{1} (p) / x]

Σ-elim_2

Γ, x : A ⊢ B type

Γ ⊢ a : A

Γ ⊢ b : B [a / x]

Γ ⊢ {pr}_{1} ((a, b)) \equiv a : A

Σ-β_1

Γ, x : A ⊢ B type

Γ ⊢ a : A

Γ ⊢ b : B [a / x]

Γ ⊢ {pr}_{2} ((a, b)) \equiv b : B [a / x]

Σ-β_2

Γ ⊢ p : \sum_{x : A} B

Γ ⊢ p \equiv ({pr}_{1} (p), {pr}_{2} (p)) : \sum_{x : A} B

Σ-η

The premise $Γ, x : A ⊢ B type$ in $Σ$ -intro and in both $β$ -rules is not recoverable from the other premises (the family $B$ is not determined by its instance $B [a / x]$ ) and is therefore displayed.

Referenced from 18 locations

For $Γ ⊢ a : A$ and $Γ ⊢ b : B [a / x]$ , the rules give $Γ ⊢ (a, b) : \sum_{x : A} B, {pr}_{1} ((a, b)) \equiv a : A, {pr}_{2} ((a, b)) \equiv b : B [a / x] .$ If $p : \sum_{x : A} B$ is a variable, neither projection computes by a $β$ -rule. The uniqueness rule instead reconstructs the whole pair: $p \equiv ({pr}_{1} (p), {pr}_{2} (p)) : \sum_{x : A} B .$

Remark 27.10 — Dependent congruence for pairs ¶

The type-former congruence has the same shape as $Π$ -form-eq. The remaining congruence rules are

Γ, x : A ⊢ B type

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

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

Γ ⊢ (a, b) \equiv (a^{'}, b^{'}) : \sum_{x : A} B

pair-eq

Γ ⊢ p \equiv p^{'} : \sum_{x : A} B

Γ ⊢ {pr}_{1} (p) \equiv {pr}_{1} (p^{'}) : A

1-eq

Γ ⊢ p \equiv p^{'} : \sum_{x : A} B

Γ ⊢ {pr}_{2} (p) \equiv {pr}_{2} (p^{'}) : B [{pr}_{1} (p) / x]

2-eq

For pair-eq, equal substitution gives $B [a / x] \equiv B [a^{'} / x]$ ; conversion along this equality moves $b^{'}$ from the displayed common fiber $B [a / x]$ to $B [a^{'} / x]$ , so the right-hand pair is well typed. For ${pr}_{2}$ -eq, rule ${pr}_{1}$ -eq gives $Γ ⊢ {pr}_{1} (p) \equiv {pr}_{1} (p^{'}) : A$ , whence $B [{pr}_{1} (p) / x] \overset{S u b s t - E q - T y}{\equiv} B [{pr}_{1} (p^{'}) / x] .$ After symmetry, this converts the second projection of $p^{'}$ to the common type shown in the conclusion.

Referenced from 4 locations

Exercise 27.7 ¶

★★☆ Restore every premise suppressed by convention 26.14 in the three rules of remark 27.10. For ${pr}_{2}$ -eq, display the Subst-Eq-Ty, Ty-Sym, and Conv steps that type the right-hand projection in the common fiber.

Referenced from 3 locations

Exercise 27.8 ¶

★☆☆ Verify, citing Subst, that the premise $Γ ⊢ b : B [a / x]$ of $Σ$ -intro is meta-well-typed: from $Γ, x : A ⊢ B type$ and $Γ ⊢ a : A$ , derive $Γ ⊢ B [a / x] type$ .

Referenced from 3 locations

Remark 27.11 — Binary products ¶

For $Γ ⊢ A type$ and $Γ ⊢ B type$ we define the product type $A \times B : = \sum_{x : A} B$ after choosing $x \notin dom (Γ)$ occurring nowhere in $B$ . Its elements are ordinary pairs. Specializing the motive of $Σ$ elimination to a constant type gives the binary-product recursor; the two projection computations and pair eta are the corresponding specializations of definition 27.9.

Referenced from 4 locations

Exercise 27.9 ¶

★★☆ Let $Γ ⊢ A type$ , $Γ ⊢ B type$ , and $Γ ⊢ C type$ . Specialize definition 27.9 to $A \times B$ (remark 27.11): display the resulting rules, define the non-dependent recursor ${rec}_{\times} (f; p) : = f ({pr}_{1} (p)) ({pr}_{2} (p))$ for $f : A \to (B \to C)$ , and verify its computation rule on pairs.

Referenced from 3 locations

Proposition 27.12 — Σ -elimination ¶

Let $Γ, z : \sum_{x : A} B ⊢ C type$ and $Γ, x : A, y : B ⊢ d : C [(x, y) / z] .$ For $Γ ⊢ p : \sum_{x : A} B$ , define ${ind}_{Σ} (d; p) : = d [{pr}_{1} (p) / x, {pr}_{2} (p) / y] .$ Then $Γ ⊢ {ind}_{Σ} (d; p) : C [p / z]$ , and on pairs the eliminator computes judgmentally: $Γ ⊢ {ind}_{Σ} (d; (a, b)) \equiv d [a / x, b / y] : C [(a, b) / z],$ for $Γ ⊢ a : A$ and $Γ ⊢ b : B [a / x]$ .

Referenced from 6 locations

[4]

Proof of Proposition 27.12 — Σ -elimination

Proof. By lemma 26.30, rename the two displayed context variables if necessary so that $x$ and $y$ occur nowhere in $Γ$ , $p$ , or $C$ . This is possible because the variables are locally declared and distinct from the domain of $Γ$ . The two projection rules give $Γ ⊢ {pr}_{1} (p) : A, Γ ⊢ {pr}_{2} (p) : B [{pr}_{1} (p) / x] .$ Thus $({pr}_{1} (p), {pr}_{2} (p))$ is a context substitution $Γ \Rightarrow (x : A, y : B)$ in the sense of definition 26.45. Applying proposition 26.46 to the derivation of $d$ gives $Γ ⊢ d [{pr}_{1} (p) / x, {pr}_{2} (p) / y] : C [({pr}_{1} (p), {pr}_{2} (p)) / z] .$ The displayed type is obtained by the defining clauses of simultaneous substitution in definition 26.10. Moreover, the simultaneous substitution agrees with two successive applications of the structural substitution rule. This follows directly by induction on $d$ : neither $x$ nor $y$ occurs in either projection of $p$ , so the two single substitutions commute at variables and the binder cases use the same fresh openings. Now symmetry of $Σ$ - $η$ gives $({pr}_{1} (p), {pr}_{2} (p)) \equiv p : \sum_{x : A} B .$ Apply Subst-Eq-Ty to the family $C$ , and then Conv; this changes the last displayed type to $C [p / z]$ . Explicitly, the classifier assembly is $\begin{aligned} C [({pr}_{1} (p), {pr}_{2} (p)) / z] & \overset{p a i r - e q, S u b s t - E q - T y}{\equiv} C [p / z], \\ d [{pr}_{1} (p) / x, {pr}_{2} (p) / y] & : C [({pr}_{1} (p), {pr}_{2} (p)) / z] \overset{C o n v}{\to} C [p / z] . \end{aligned}$

For the computation equation, put $q_{1} : = {pr}_{1} ((a, b)), q_{2} : = {pr}_{2} ((a, b)) .$ The two beta rules give $q_{1} \equiv a : A$ and $q_{2} \equiv b : B [a / x]$ ; equal substitution along the first equality converts the original type $B [q_{1} / x]$ of $q_{2}$ to $B [a / x]$ . Apply Subst-Eq-Tm at $x : A$ and then substitute $q_{2}$ for $y$ . Its common context is the one based on $q_{1}$ , and it gives $d [q_{1} / x, q_{2} / y] \equiv d [a / x, q_{2} / y] : C [(q_{1}, q_{2}) / z] .$ Separately, apply Subst-Eq-Tm at $y : B [a / x]$ to the already substituted term $d [a / x]$ : $d [a / x, q_{2} / y] \equiv d [a / x, b / y] : C [(a, q_{2}) / z] .$ Rule pair-eq gives $(q_{1}, q_{2}) \equiv (a, q_{2})$ , using reflexivity for $q_{2}$ in the common fiber. Equal substitution in $C$ and Conv-Eq therefore type the two steps in one fiber: $d [q_{1} / x, q_{2} / y] \overset{S u b s t - E q - T m, C o n v - E q}{=} d [a / x, q_{2} / y] \overset{S u b s t - E q - T m}{=} d [a / x, b / y] : C [(a, q_{2}) / z] .$ A second use of pair-eq, this time with $q_{2} \equiv b$ , gives $(a, q_{2}) \equiv (a, b)$ . Equal substitution in $C$ and Conv-Eq place the chain in $C [(a, b) / z]$ , as required. ◻

Proposition 27.13 — The positive presentation ¶

The negative presentation of definition 27.9 derives the positive eliminator and computation rule of proposition 27.12. Conversely, the positive presentation consisting of formation, pairing, the primitive eliminator ${ind}_{Σ}$ of arity $(2, 0)$ , and its pair computation derives both projections and their beta rules. If Sigma eta is added to the positive presentation, the two presentations are interderivable.

Referenced from 4 locations

Dependent Products, Sums, and Unit

Proof of Proposition 27.13 — The positive presentation

Proof. The negative-to-positive direction is proposition 27.12. For the converse, the first projection is the constant-motive instance ${pr}_{1} (p) : = {ind}_{Σ} (x; p), C : = A in context z : \sum_{x : A} B .$ After this definition, take the motive $C : = B [{pr}_{1} (z) / x]$ and the branch $y$ . The branch has the required type because the first projection computes on $(x, y)$ . Equal substitution gives $B [{pr}_{1} ((x, y)) / x] \equiv B .$ After symmetry, conversion types $y : B$ in the left-hand type. This defines ${pr}_{2} (p)$ , and the primitive computation rule gives both projection beta rules.

Adding Sigma eta supplies the only remaining rule of the negative presentation. Thus every rule of either presentation is admissible in the other, although their primitive raw operators remain different. ◻

Remark 72.14 ¶

If $p$ is a variable, ${ind}_{Σ} (-; p)$ has no computation step. Therefore the positive computation rule alone does not derive $p \equiv ({pr}_{1} (p), {pr}_{2} (p))$ ; this is exactly the additional eta equation assumed in the final clause of remark 27.13.

The terminology collides across the simple/dependent divide: $Π$ -types generalize function types yet are called dependent products, while $Σ$ -types generalize product types yet are called dependent sums. The set-theoretic reading resolves the puzzle: $\prod_{a \in A} B_{a}$ is an $A$ -indexed product of sets whose elements are (choice) functions, and $\underset{a \in A}{∐} B_{a}$ is an $A$ -indexed sum (disjoint union) whose elements are pairs of an index with an inhabitant. Both specialize to the binary product: $B_{1} \times B_{2}$ is the product indexed by ${1, 2}$ and also the sum of the constant family $B_{2}$ indexed by $B_{1}$ .

Exercise 27.10 ¶

★★★ In the positive presentation of remark 27.13, write the complete derivation of the second projection. In context $z : \sum_{x : A} B$ , use the motive $C : = B [{pr}_{1} (z) / x]$ ; display the conversion that types the branch $y$ , and verify the beta rule. Finally explain why the primitive computation rule has no computation step when the scrutinee is an arbitrary variable $p$ , and hence does not derive $p \equiv ({pr}_{1} (p), {pr}_{2} (p))$ .

Referenced from 3 locations

The unit type

The unit type is the nullary product. Its constructor $⋆$ contains no components, and its $η$ -rule gives $a \equiv ⋆ : 1$ for every $a : 1$ . Consequently a function $f : 1 \to B$ is determined by $f ⋆$ : for any $a : 1$ , congruence sends $a \equiv ⋆$ to $f a \equiv f ⋆$ . Both $1$ and $⋆$ are nullary raw operators.

Definition 27.14 — Rules for ¶

The unit type is given by the following rules; congruence rules are tacit.

Γ ctx

Γ ⊢ 1 type

-form

Γ ctx

Γ ⊢ ⋆ : 1

-intro

Γ ⊢ a : 1

Γ ⊢ a \equiv ⋆ : 1

-η

Referenced from 9 locations

Lemma 27.15 — Scoping in the extended theory ¶

For every expression judgment $Γ ⊢ J$ derivable after adding the $Π$ -, $Σ$ -, and $1$ -rules, every free variable displayed in $J$ belongs to $dom (Γ)$ . In a derivable context, the free variables of each declaration type belong to the preceding prefix.

Referenced from 3 locations

Dependent Products, Sums, and Unit

Proof of Lemma 27.15 — Scoping in the extended theory

Proof. Proceed simultaneously over derivations of contexts and of the four expression judgments. In the structural cases, Var selects a declared name; Wk only enlarges the domain; and Subst replaces $x$ by the substituend, whose free variables already lie in the prefix $Γ$ . Context conversion and the equality rules change no free variables. For a representative new binder case, the premise of $Π$ -introduction has $FV (b) \subseteq dom (Γ) \cup {x}$ ; abstraction binds $x$ , so $FV (λ (x : A) . b) \subseteq dom (Γ)$ , using also $FV (A) \subseteq dom (Γ)$ . The formation rules for $Π$ and $Σ$ have the same binder calculation. For application, the representative non-binder equation is $FV (f a) = FV (f) \cup FV (a) \subseteq dom (Γ) .$ Pairing and projection take the same union of the free-variable sets of their premises, while the nullary $1$ and $⋆$ retain none. Computation, uniqueness, and congruence compare expressions satisfying these same inclusions. ◻

By $1$ -intro, in every well-formed context the judgment $Γ ⊢ ⋆ : 1$ is derivable. If a context also contains a variable $u : 1$ , no reduction rule acts on $u$ , but uniqueness gives the immediate calculation $Γ, u : 1 ⊢ u \equiv ⋆ : 1 .$

Remark 27.16 — No elimination rule ¶

Definition 27.14 contains no elimination rule and no $β$ -rule. None is needed: every $a : 1$ is judgmentally $⋆$ . Conversion along $a \equiv ⋆$ therefore derives the dependent eliminator in proposition 27.17.

Referenced from 2 locations

Dependent Products, Sums, and Unit

Proposition 27.17 — The dependent eliminator for ¶

Let $Γ, z : 1 ⊢ C type$ , let $Γ ⊢ c : C [⋆ / z]$ , and let $Γ ⊢ a : 1$ . Define ${ind}_{1} (c; a) : = c$ . Then $Γ ⊢ {ind}_{1} (c; a) : C [a / z]$ , and $Γ ⊢ {ind}_{1} (c; ⋆) \equiv c : C [⋆ / z]$ .

Referenced from 7 locations

Proof of Proposition 27.17 — The dependent eliminator for

Proof. By $1$ - $η$ , $a \equiv ⋆ : 1$ . Apply Tm-Sym first, so $⋆ \equiv a : 1$ . Then Subst-Eq-Ty for the family $C$ gives $C [⋆ / z] \equiv C [a / z] type .$ Rule Conv converts $c : C [⋆ / z]$ to $c : C [a / z]$ , which is the typing claim. The computation equation is reflexivity. ◻

Remark 27.18 — The eta convention ¶

In the calculus of definition 27.2, definition 27.9, definition 27.14, the three $η$ -equations are primitive judgmental equalities. They do not follow from the corresponding $β$ -rules. Unit eta converts the constant branch into the fiber over an arbitrary unit term in proposition 27.17. Sigma eta types the dependent uncurrying map and supplies the reassociation conversions. Pi eta closes the function round trips for currying and the categorical unit laws.

Referenced from 2 locations

Dependent Products, Sums, and Unit

Exercise 27.11 ¶

★☆☆ Given $Γ ⊢ f : 1 \to 1$ and $Γ ⊢ g : 1 \to 1$ , show $f \equiv g$ and conclude $f \equiv {id}_{1}$ . Which $η$ -rules does the argument use?

Referenced from 3 locations

Exercise 27.12 ¶

★☆☆ Write out the proof of proposition 27.17 as a derivation tree, citing Tm-Sym, Subst-Eq-Ty, and Conv at the exact steps where they occur.

Referenced from 3 locations

Internalizing judgmental structure

The introduction and elimination rules move in opposite directions. The eta rules say that, after quotienting by judgmental equality, these moves are inverse.

Definition 27.19 — Term sets ¶

Let $Γ ctx$ and $Γ ⊢ A type$ . Define $Tm (Γ, A) : = {a ∣ Γ ⊢ a : A derivable} / \equiv$ to be the set of terms of $A$ in context $Γ$ , taken modulo judgmental equality. If $A \equiv A^{'}$ as types, Conv in both directions gives the same term representatives, and Conv-Eq in both directions gives the same equivalence relation. We therefore identify $Tm (Γ, A)$ with $Tm (Γ, A^{'})$ .

Here “set” has its metatheoretic meaning from convention 71.1. The raw expressions form a set, the displayed collection is a subset, and quotienting by derivable judgmental equality therefore produces a set. The symbol $\sum$ below denotes the corresponding metatheoretic disjoint union, not an object-language $Σ$ -type.

Referenced from 3 locations

Dependent Products, Sums, and Unit

Proposition 27.20 — term classes ¶

If $Γ ctx$ , then $Tm (Γ, 1)$ is a singleton.

Referenced from 3 locations

Dependent Products, Sums, and Unit

Proof of Proposition 27.20 — term classes

Proof. It contains $[⋆]$ by $1$ -intro. If $[a]$ is any other element, $1$ - $η$ gives $a \equiv ⋆$ , hence $[a] = [⋆]$ . ◻

Theorem 27.21 — Π internalizes the hypothetical judgment ¶

Let $Γ ⊢ A type$ and $Γ, x : A ⊢ B type$ . Define $Λ (b) : = λ (x : A) . b and E (f) : = f x,$ where $E$ first weakens $f$ to $Γ, x : A$ (definition 26.21) and applies it to the variable $x$ . Then:

$Λ$ and $E$ preserve judgmental equality, and induce mutually inverse bijections $Tm ((Γ, x : A), B) ≅ Tm (Γ, \prod_{x : A} B);$
both maps commute with substitution. More precisely, if $Γ = Γ_{0}, y : C, Γ_{1}$ , if $Γ_{0} ⊢ c : C$ , and if $Γ [c / y]$ abbreviates $Γ_{0}, Γ_{1} [c / y]$ , then $Λ (b) [c / y] = Λ (b [c / y]), E (f) [c / y] = E (f [c / y])$ as equalities of expression classes. The first lies in $Tm (Γ [c / y], \prod_{x : A [c / y]} B [c / y]),$ and the second is an equality of terms of $B [c / y]$ in the context $Γ [c / y], x : A [c / y]$ .

Referenced from 9 locations

Proof of Theorem 27.21 — Π internalizes the hypothetical judgment

Proof. (1) Preservation of $\equiv$ is $λ$ -eq and app-eq. For the round trips, let $Γ, x : A ⊢ b : B$ and choose $x^{'} \neq x$ occurring nowhere in $Γ, A, B, b$ . Choose the alpha-equivalent representative with binder $x^{'}$ . Then, in $Γ, x : A$ , $E (Λ (b)) = (λ (x^{'} : A) . b [x^{'} / x]) x \equiv b [x^{'} / x] [x / x^{'}] = b .$ The beta rule gives the judgmental step. The final raw equality follows by structural induction on that representative of $b$ : the second substitution reverses precisely the occurrences changed by the first. Conversely, for $Γ ⊢ f : \prod_{x : A} B$ , $Λ (E (f)) = λ (x : A) . f x \equiv f$ by $Π$ - $η$ . Hence the induced maps on $\equiv$ -classes are mutually inverse.

(2) The context formation makes $x \neq y$ . By lemma 27.15, $FV (c) \subseteq dom (Γ_{0})$ , hence $x \notin FV (c)$ . Choose representatives whose other bound names avoid $y$ and $FV (c)$ . The operator clauses of definition 26.10 then give $\begin{aligned} (λ (x : A) . b) [c / y] & = λ (x : A [c / y]) . b [c / y], \\ (f x) [c / y] & = f [c / y] x . \end{aligned}$ Weakening does not change the raw representative of $f$ , so these are the two asserted equations in the substituted contexts. ◻

Theorem 27.22 — Σ internalizes pairs of judgments ¶

Let $Γ ⊢ A type$ and $Γ, x : A ⊢ B type$ . There is a bijection $Tm (Γ, \sum_{x : A} B) ≅ \sum_{a \in Tm (Γ, A)} Tm (Γ, B [a / x]),$ given on representatives by $F (p) = ({pr}_{1} (p), {pr}_{2} (p)), G (a, b) = (a, b) .$ The fiber on the right is independent of the representative of $a$ via the identification in definition 27.19. The two maps also commute with substitution in the sense of theorem 27.21(2): under the hypotheses there, substitution acts componentwise and $F ([p]) [c / y] = F ([p [c / y]]), G ([a], [b]) [c / y] = G ([a [c / y]], [b [c / y]]) .$

Referenced from 4 locations

Proof of Theorem 27.22 — Σ internalizes pairs of judgments

Proof. We first make the dependent quotient precise. If $a \equiv a^{'} : A$ , then Subst-Eq-Ty gives $B [a / x] \equiv B [a^{'} / x] type .$ By Conv, the two fibers have the same term representatives; by Conv-Eq, they have the same equality classes. Hence the fiber $Tm (Γ, B [a / x])$ depends only on $[a]$ .

The forward map lands in this fiber because ${pr}_{1} (p) : A, {pr}_{2} (p) : B [{pr}_{1} (p) / x] .$ If $p \equiv p^{'}$ , the rules ${pr}_{1}$ -eq and ${pr}_{2}$ -eq show that both resulting classes agree, with the second equality taken in the common fiber over $[{pr}_{1} (p)]$ . Thus $F$ is well defined.

For $G$ , suppose $a \equiv a^{'} : A$ and that $b$ and $b^{'}$ determine the same class after identifying $B [a / x]$ with $B [a^{'} / x]$ . In the common fiber we have $b \equiv b^{'} : B [a / x]$ , so pair-eq gives $(a, b) \equiv (a^{'}, b^{'}) : \sum_{x : A} B .$ Thus $G$ too is independent of representatives.

The two beta rules give $F (G ([a], [b])) = ([a], [b]),$ and symmetry of $Σ$ - $η$ gives $G (F ([p])) = [({pr}_{1} (p), {pr}_{2} (p))] = [p] .$ The maps are therefore inverse.

Finally, under the context-substitution hypotheses of theorem 27.21(2), the operator clauses of definition 26.10 give $\begin{aligned} {pr}_{i} (p) [c / y] & = {pr}_{i} (p [c / y]) (i = 1, 2), \\ (a, b) [c / y] & = (a [c / y], b [c / y]) . \end{aligned}$ These are exactly the two naturality equations. For the dependent second component, the identification of the substituted fibers is the calculation $(B [a / x]) [c / y] = B [c / y] [a [c / y] / x],$ which follows from $x \neq y$ , $x \notin FV (c)$ , and proposition 26.11.4. Thus both sides really do lie in the same displayed fiber. ◻

Remark 27.23 — The slogan ¶

These three results have one form: each type packages structure already expressible with judgments. $\begin{aligned} Tm (Γ, \prod_{x : A} B) & ≅ Tm (Γ, x : A; B), \\ Tm (Γ, \sum_{x : A} B) & ≅ \sum_{[a] \in Tm (Γ, A)} Tm (Γ, B [a / x]), \\ Tm (Γ, 1) & ≅ {*} . \end{aligned}$ Here $Tm (Γ, x : A; B)$ abbreviates the term classes of $B$ in the extended context; the semicolon prevents it from being mistaken for a two-argument term-set notation.

Referenced from 2 locations

Dependent Products, Sums, and Unit

Exercise 27.13 ¶

★☆☆ Specialize theorem 27.22 to a constant family and obtain a bijection $Tm (Γ, A \times B) ≅ Tm (Γ, A) \times Tm (Γ, B) .$ Write the two maps and both round trips explicitly.

Referenced from 3 locations

Exercise 27.14 ¶

★☆☆ Verify theorem 27.21(2) directly from the defining clauses of substitution in definition 26.10, indicating exactly where the freshness of $x$ for $y$ and $c$ is used.

Referenced from 3 locations

Exercise 27.15 ¶

★☆☆ Formulate and prove the analogue of theorem 27.21(2) for the unit type: the bijection of proposition 27.20 commutes with substitution. What do the two composite maps look like concretely?

Referenced from 3 locations

Exercise 27.16 ¶

★★★ (Internalization reconstructs the term rules.) Fix $Γ ⊢ A type$ and $Γ, x : A ⊢ B type$ , and suppose $Γ ⊢ P type$ is a type equipped with alpha-respecting raw-term operations $Λ^{'}$ and $E^{'}$ . They are accompanied by derivation transformations sending each derivation of $Γ, x : A ⊢ b : B$ to one of $Γ ⊢ Λ^{'} (b) : P$ and each derivation of $Γ ⊢ f : P$ to one of $Γ, x : A ⊢ E^{'} (f) : B$ . Assume that the raw operations commute with substitution, their transformations send equality derivations to equality derivations, and they come with derivations $E^{'} (Λ^{'} (b)) \equiv b : B, Λ^{'} (E^{'} (f)) \equiv f : P .$ Use $Λ^{'}$ as introduction and define elimination by $f a : = E^{'} (f) [a / x]$ . Derive the beta rule by substituting $a$ into the first displayed equality, derive eta from the second, and derive the two congruence rules from equality preservation and Subst-Eq-Tm. The formation rule is the assumed judgment $Γ ⊢ P type$ .

Referenced from 3 locations

Definitional isomorphisms

Two types can be carried into each other by maps whose round trips are judgmentally the identity. The $η$ -rules make such round trips collapse; currying and the associativity of $Σ$ are the two cases needed below.

Definition 27.24 — Definitional isomorphism ¶

Let $Γ ⊢ A type$ and $Γ ⊢ B type$ . A definitional isomorphism $A ≅ B$ consists of terms $Γ ⊢ f : A \to B$ and $Γ ⊢ g : B \to A$ such that ${x, y} \cap dom (Γ) = \emptyset$ and $x \neq y$ , and $Γ, x : A ⊢ g (f x) \equiv x : A and Γ, y : B ⊢ f (g y) \equiv y : B .$ Equivalently, $g \circ f \equiv {id}_{A}$ and $f \circ g \equiv {id}_{B}$ . Indeed, abstraction congruence turns the two displayed equations into these equations of functions. Conversely, apply the first functional equation to $x$ and the second to $y$ , use app-eq, and reduce both sides by $β$ . Here $≅$ relates two object-language types and requires judgmental round trips. The same printed glyph in theorem 27.21 relates metatheoretic sets of term classes by an ordinary bijection.

Referenced from 4 locations

Dependent Products, Sums, and Unit

Proposition 27.25 — Currying ¶

Let $Γ ⊢ A type$ , $Γ, x : A ⊢ B type$ , and $Γ, p : \sum_{x : A} B ⊢ C type$ . Choose the displayed binders $x, p, y, f, g, w$ pairwise fresh, disjoint from $dom (Γ)$ , and put $P : = \prod_{p : \sum_{x : A} B} C, Q : = \prod_{x : A} \prod_{y : B} C [(x, y) / p] .$ There is a definitional isomorphism $P ≅ Q$ given by $Φ : = λ (f : P) . λ (x : A) . λ (y : B) . f ((x, y)),$ $Ψ : = λ (g : Q) . λ (w : \sum_{x : A} B) . g ({pr}_{1} (w)) ({pr}_{2} (w)) .$

Referenced from 7 locations

Proof of Proposition 27.25 — Currying

Proof. First check the typing. For $Φ$ , given $f : P$ , $x : A$ , and $y : B$ , rule $Σ$ -intro gives $(x, y) : \sum_{x : A} B$ . Hence $f ((x, y)) : C [(x, y) / p]$ , and three abstractions finish.

For $Ψ$ , let $g : Q$ and $w : \sum_{x : A} B$ . Substitution in the product type gives $g ({pr}_{1} (w)) : \prod_{y : B [{pr}_{1} (w) / x]} C [({pr}_{1} (w), y) / p],$ by definition 26.10. Applying this term to ${pr}_{2} (w)$ gives $g ({pr}_{1} (w)) ({pr}_{2} (w)) : C [({pr}_{1} (w), {pr}_{2} (w)) / p] .$ Symmetry of $Σ$ - $η$ gives $({pr}_{1} (w), {pr}_{2} (w)) \equiv w$ , whence $C [({pr}_{1} (w), {pr}_{2} (w)) / p] \overset{S u b s t - E q - T y}{\equiv} C [w / p] .$ Rule Conv therefore gives the body the required type $C [w / p]$ in the context $Γ, w : \sum_{x : A} B$ .

Round trip on $f$ : in context $Γ, f : P$ , $\begin{aligned} Ψ (Φ f) & \overset{Π - β}{\equiv} λ (p : \sum_{x : A} B) . Φ f ({pr}_{1} (p)) ({pr}_{2} (p)) \\ \overset{Π - β, λ - e q}{\equiv} λ (p : \sum_{x : A} B) . f (({pr}_{1} (p), {pr}_{2} (p))) \\ \overset{Σ - η, a p p - e q, λ - e q}{\equiv} λ (p : \sum_{x : A} B) . f p \\ \overset{Π - η}{\equiv} f . \end{aligned}$ Round trip on $g$ : in the corresponding context, $\begin{aligned} Φ (Ψ g) & \overset{Π - β}{\equiv} λ (x : A) . λ (y : B) . Ψ g ((x, y)) \\ \overset{Π - β, λ - e q}{\equiv} λ (x : A) . λ (y : B) . g ({pr}_{1} ((x, y))) ({pr}_{2} ((x, y))) \\ \overset{Σ - β, a p p - e q, λ - e q}{\equiv} λ (x : A) . λ (y : B) . g x y \\ \overset{Π - η, λ - e q}{\equiv} g . \end{aligned}$ The last step uses $Π$ - $η$ first under the inner abstraction and then under the outer one, both in the symmetric direction; $λ$ -eq carries the inner equality through the outer binder. ◻

Proposition 27.26 — Associativity of Σ ¶

Let $Γ ⊢ A type$ , $Γ, x : A ⊢ B type$ , and $Γ, p : \sum_{x : A} B ⊢ C type$ . There is a definitional isomorphism $\sum_{p : \sum_{x : A} B} C ≅ \sum_{x : A} \sum_{y : B} C [(x, y) / p]$

Referenced from 4 locations

Proof of Proposition 27.26 — Associativity of Σ

Proof. Take the comparison maps $\begin{aligned} Θ & : = λ (q : \sum_{p : \sum_{x : A} B} C) . ({pr}_{1} ({pr}_{1} (q)), ({pr}_{2} ({pr}_{1} (q)), {pr}_{2} (q))), \\ Ξ & : = λ (r : \sum_{x : A} \sum_{y : B} C [(x, y) / p]) . (({pr}_{1} (r), {pr}_{1} ({pr}_{2} (r))), {pr}_{2} ({pr}_{2} (r))) . \end{aligned}$ For the typing of $Θ$ : given $q$ in the left-hand type, ${pr}_{2} (q) : C [{pr}_{1} (q) / p]$ . Put $s : = {pr}_{1} (q)$ . Equal substitution applied to $s \equiv ({pr}_{1} (s), {pr}_{2} (s))$ gives the short conversion $C [s / p] \equiv C [({pr}_{1} (s), {pr}_{2} (s)) / p] .$ This places ${pr}_{2} (q)$ in the type required for the inner pair; record the converted judgment as $Γ, q : \sum_{p : \sum_{x : A} B} C ⊢ {pr}_{2} (q) : C [({pr}_{1} (s), {pr}_{2} (s)) / p] .$ The typing of $Ξ$ needs no conversion.

For the first round trip, beta-reduce the two maps and their projections: $\begin{aligned} Ξ (Θ q) & \overset{Π - β, Σ - β}{\equiv} (({pr}_{1} (s), {pr}_{2} (s)), {pr}_{2} (q)) \\ \overset{(72.1), p a i r - e q}{\equiv} (s, {pr}_{2} (q)) \\ \overset{Σ - η}{\equiv} q . \end{aligned}$ For the other, put $t : = {pr}_{2} (r)$ . Then $\begin{aligned} Θ (Ξ r) & \overset{Π - β, Σ - β}{\equiv} ({pr}_{1} (r), ({pr}_{1} (t), {pr}_{2} (t))) \\ \overset{Σ - η, p a i r - e q}{\equiv} ({pr}_{1} (r), t) \\ \overset{Σ - η}{\equiv} r . \end{aligned}$ No corresponding fiber conversion is needed in this second chain: the two outer pairs have the identical first component ${pr}_{1} (r)$ . Thus $Θ$ and $Ξ$ satisfy definition 27.24. ◻

Remark 27.27 — Strength of the notion ¶

Judgmental equality of types is sufficient for a definitional isomorphism: if $A \equiv B$ , conversion types the identity abstraction in both directions. The converse fails, however: inverse comparison maps and their equations do not constitute a judgmental equality of the two type expressions. The eta rules play different roles. Without $Σ$ -eta, the uncurrying map $Ψ$ of example 27.25 and the eliminator of proposition 27.12 are not well typed: their bodies lie over $({pr}_{1} (p), {pr}_{2} (p))$ and must be converted to the fiber over $p$ . $Σ$ -eta is used again in both associativity round trips and in the third step of the currying round trip on $f$ . By contrast, $Π$ -eta is used in the round trips: at the final step of each currying composite and in the unit laws of lemma 27.7.

Referenced from 2 locations

Dependent Products, Sums, and Unit

Lemma 27.28 — Calculus of definitional isomorphisms ¶

The identity maps give $A ≅ A$ ; reversing the two maps gives an inverse isomorphism; and definitional isomorphisms compose. Composition is associative and has the identity isomorphisms as units, up to judgmental equality of the comparison maps.

Referenced from 2 locations

Dependent Products, Sums, and Unit

Proof of Lemma 27.28 — Calculus of definitional isomorphisms

Proof. Only composition needs calculation. Let $f : A \to B$ and $g : B \to A$ be one inverse pair, and let $f^{'} : B \to C$ and $g^{'} : C \to B$ be another. The composite pair is $f^{'} \circ f : A \to C$ and $g \circ g^{'} : C \to A$ . For $x : A$ , beta unfolds the two composites. Name the pointwise inverse equations $\begin{aligned} (I_{A}) & g (f x) & \equiv x, \\ (I_{B}) & f (g y) & \equiv y, \\ (I_{B}^{'}) & g^{'} (f^{'} y) & \equiv y, \\ (I_{C}) & f^{'} (g^{'} z) & \equiv z . \end{aligned}$ Then $\begin{aligned} (g \circ g^{'}) ((f^{'} \circ f) x) & \overset{Π - β}{\equiv} g (g^{'} (f^{'} (f x))) \\ \overset{(I_{B}^{'}), a p p - e q}{\equiv} g (f x) \\ \overset{(I_{A})}{\equiv} x . \end{aligned}$ The middle step substitutes $f x$ for $y$ in the inverse hypothesis $g^{'} (f^{'} y) \equiv y$ and then uses app-eq under $g$ ; the last step is the other inverse hypothesis $g (f x) \equiv x$ . The calculation at $z : C$ is the same in the other order: $(f^{'} \circ f) ((g \circ g^{'}) z) \overset{Π - β, (I_{B})}{\equiv} f^{'} (g^{'} z) \overset{(I_{C})}{\equiv} z .$ The identity and inverse pairs are immediate from definition 27.24; the associative and unit equations for their comparison maps are precisely lemma 27.7. ◻

Exercise 27.17 ¶

★★☆ Verify directly from definition 26.10 that the maps $Θ$ and $Ξ$ of example 27.26 commute with substitution in every variable of $Γ$ .

Referenced from 3 locations

Exercise 27.18 ¶

★★★ Assume $Γ ⊢ A type$ , and construct definitional isomorphisms $\sum_{x : A} 1 ≅ A and \prod_{x : 1} B ≅ B [⋆ / x],$ the latter for any family $Γ, x : 1 ⊢ B type$ . For the second map, use $x \equiv ⋆$ to convert an element of $B [⋆ / x]$ to an element of $B$ , then abstract over $x$ . Identify precisely which eta rules the two round trips use.

Referenced from 3 locations

Exercise 27.19 ¶

★☆☆ Specialize example 27.25 to constant families to obtain the definitional isomorphism $(A \times B) \to C ≅ A \to (B \to C)$ , and check that the specialized maps agree with the classical $λ^{\to}$ combinators $\begin{aligned} curry & : = λ (f : (A \times B) \to C) . λ (x : A) . λ (y : B) . f ((x, y)), \\ uncurry & : = λ (g : A \to (B \to C)) . λ (p : A \times B) . g ({pr}_{1} (p)) ({pr}_{2} (p)) . \end{aligned}$

Referenced from 3 locations

Suggested first pass.

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

Exercise 72.20 ¶

★★☆ Starting only from the positive $Σ$ -eliminator and its computation rule, derive both projections and their two computation equations. Conversely, starting from projections, their computation equations, and judgmental $Σ$ -eta, reconstruct the positive eliminator. Mark the exact step in the second direction at which $Σ$ -eta is used.

Referenced from 4 locations

Exercise 72.21 ¶

★★☆ Reconstruct the two maps of dependent currying and annotate every step of both round trips by the $Π$ - or $Σ$ -computation and uniqueness rule used. Give one family for which replacing judgmental $Σ$ -eta by a propositional equality would weaken the conclusion.

Referenced from 3 locations

Exercise 72.22 ¶

★★☆ Work in the freely generated $Π$ - $Σ$ theory with the beta rules but without judgmental $Σ$ -eta. For a neutral variable $p : \sum_{x : A} B$ , compare the beta-normal forms of $p$ and $({pr}_{1} (p), {pr}_{2} (p))$ . Use this comparison to locate the stalled step in the uncurry–curry round trip. What conclusion remains if one adds only a propositional $Σ$ -eta witness?

Referenced from 3 locations

Exercise 72.23 ¶

★★★ Practical project.pisigma-rule-checker Implement in Agda or Kappa a checker for the $Π$ , $Σ$ , and $1$ rules on explicitly annotated terms. Preserve the invariant that every returned type is well formed in the input context. It must accept the dependent curry/uncurry maps and reject a second projection whose family is indexed by a different first component; print the inferred type or the first failed premise. Before implementing the checker, run the same two tests as derivation trees: derive the type of dependent curry and mark the first ill-typed premise of the mismatched projection. These trees specify the checker’s accepted and rejected results.

Referenced from 5 locations

Sources. Dependent products and sums, the fourfold rule order, and their meaning explanations are developed in [ML98, ML75, ML84, ML96]; textbook accounts include [NPS90, NPS00, Tho91]. Internalization is emphasized in [AG26, Hof97] and has the categorical form described in [Jac99, Dyb96]. The HoTT Book gives positive $Σ$ -elimination without judgmental $Σ$ -eta [Uni13].