ch:dependent-intersections: dependent intersections

Elimination gives $left (d) : A$ and $right (d) : B$ . Both projections erase to $erase (d)$ , so DI-I gives $both (left (d), right (d)) : x : A \cap B$ . The two beta rules return the two displayed projections, and DI- $η$ identifies the rebuilt view with $d$ . The same-erasure premise is discharged by the two projection erasure equations.

Ordinary intersection permits no dependency but both eliminations return the same subject; taking a would-be body $B (x)$ exhibits the missing dependency. A dependent sum permits dependency but its projections erase to distinct pair projections, as witnessed by $(0, refl)$ . A refinement ${x : A ∣ P (x)}$ permits $P$ to mention $x$ and returns the data subject, but proof elimination returns the stored certificate rather than that same erasure. Dependent intersection permits the dependency and both views erase to one program. The rejected term $both (λ x . x, λ x .0)$ shows that dependency alone does not waive its same-subject premise.

Let $A$ be the carrier view, $B (r)$ the multiplication view, and $C (r)$ the view containing $e : r . car$ and the two equations $r . mul (e, x) = x$ and $r . mul (x, e) = x$ . The type is $r : A \cap (b : B (r) \cap C (r, b))$ . The natural instance is one label function $s$ , annotated successively as the carrier $N$ , addition, and unit $0$ with the two arithmetic proofs. Every intersection projection erases to $s$ ; field selection alone chooses a label branch.

Semantically, the left association says $R_{A} (t, t^{'}) \land (R_{B} (t, t^{'}) \land R_{C} (t, t^{'}))$ and the right association says $(R_{A} (t, t^{'}) \land R_{B} (t, t^{'})) \land R_{C} (t, t^{'})$ . Propositional associativity gives equivalence. Functionality of $B$ and $C$ ensures that changing a related representative does not change either later conjunct.

Expanding equation 93.1 on the left gives $R_{A} (t, t^{'}) \land R_{B}^{t, t^{'}} (t, t^{'}) \land R_{C}^{t, t^{'}} (t, t^{'}) .$ Expanding the outer and inner intersections on the right gives the identical three conjuncts, parenthesized oppositely. Associativity of conjunction therefore proves extensional equality. When the inner representative changes from $t$ to $u$ with $R_{A} (t, u)$ , functionality supplies equality of the $B$ -fiber; related $B$ representatives then supply equality of the $C$ -fiber. Without those two transports the third conjunct would be representative dependent.

For DI-I, the two typing premises place the common erasure class $E$ in $R_{A}$ and in the selected $R_{B}^{E}$ ; the erasure premise identifies the two classes, so their conjunction holds. For DI-E $_{2}$ , intersection membership selects the $R_{B}$ conjunct, while the first projection chooses the same representative used in its fiber. Substitution commutes with both conjuncts; in the second it also substitutes in the family index, and functionality identifies the resulting fibers.

If functionality is removed, take related $a, a^{'}$ in $R_{A}$ but define $B (a)$ to be the total PER and $B (a^{'})$ the empty PER. A subject $t$ can then satisfy the second conjunct under $a$ but not under $a^{'}$ . Thus elimination and substitution depend on the representative and validation fails.