These notes are being changed!!!

Index of the slides:

Preservation of ‘true’ and ‘and’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Preservation of ‘implies’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 BCC for ‘forall’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 BCC for ‘exists’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 BCC for equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 Frobenius for ‘exists’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Frobenius for equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 BCC, categorically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 BCC in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 BCC: collapsing isomorphic objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 BCC for dependent sums: full diagram . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 BCC: smaller diagram . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 BCC: smaller diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 BCC: trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Preservation of ‘true’ and ‘and’

[figure: ⊤; ⊤; ⊤; ⊤; ♮; ⊤; ⊤; P⊤; a; b; P; P; P; P &Q; P; P &Q; P; P &Q; P &Q; P &Q; ♮; P &Q; P &Q; P&; P &Q; P &Q; P &Q; Q; P &Q; Q; P &Q; Q; Q; Q; a; b]

[figure: f^{∗}⊤_{B}; ⊤_{B}; f^{∗}⊤_{B}; ⊤_{A}; ♮; f^{∗}⊤_{B}; ⊤_{A}; P⊤; A; B; f; f^{∗}P; P; f^{∗}P; f^{∗}P &f^{∗}Q; f^{∗}P; f^{∗}(P &Q); P; P &Q; f^{∗}P &f^{∗}Q; f^{∗}(P &Q); ♮; f^{∗}P &f^{∗}Q; f^{∗}(P &Q); P&; f^{∗}(P &Q); P &Q; f^{∗}P &f^{∗}Q; f^{∗}Q; f^{∗}(P &Q); f^{∗}Q; P &Q; Q; f^{∗}Q; Q; A; B; f]

Preservation of ‘implies’

(P [figure]Q)&P  (P [figure]Q)&P [figure] ^{♮} (P [figure]Q)&P  (P [figure]Q)&P_{P&} [figure] (P [figure]Q)&P  (P [figure]Q)&P [figure] (P [figure]Q)&P Q[figure]  (P [figure]Q)&P Q [figure] [figure]  (P [figure]Q)&P Q[figure] Q  Q [figure] (P [figure]Q)&P  P [figure]Q [figure] [figure] Q  P [figure]Q [figure] [figure]  (P [figure]Q)&P  P [figure]Q [figure] [figure] Q  P [figure]Q [figure] [figure] P [figure]Q  P [figure]Q [figure]  P [figure]Q P [figure]Q_{id} [figure] P [figure]Q P [figure]Q_{♮} [figure] P [figure]Q P [figure]Q [figure]_{P [figure]} [figure] [figure] [figure]  [figure] [figure] a  b [figure]

f^{∗}(P [figure]Q)&f^{∗}P  f^{∗}((P [figure]Q)&P) [figure]^{♮} f^{∗}(P [figure]Q)&f^{∗}P  f^{∗}((P [figure]Q)&P)_{P&} [figure] f^{∗}((P [figure]Q)&P)  (P [figure]Q)&P [figure] f^{∗}(P [figure]Q)&f^{∗}P f^{∗}Q [figure]  f^{∗}((P [figure]Q)&P) f^{∗}Q [figure] [figure]  (P [figure]Q)&P Q[figure] f^{∗}Q  Q [figure] f^{∗}(P [figure]Q)&f^{∗}P  f^{∗}(P [figure]Q) [figure] [figure] f^{∗}Q  f^{∗}P [figure]f^{∗}Q [figure] [figure]  (P [figure]Q)&P  P [figure]Q [figure] [figure] Q  P [figure]Q [figure] [figure] f^{∗}(P [figure]Q)  P [figure]Q [figure]  P [figure]Q P [figure]Q_{id} [figure] f^{∗}(P [figure]Q) f^{∗}P [figure]f^{∗}Q_{♮} [figure] f^{∗}(P [figure]Q) f^{∗}P [figure]f^{∗}Q [figure]_{P [figure]} [figure] [figure] [figure]  [figure] [figure] A  B_{f}  [figure]

BCC for ‘forall’

[figure: ∀c.P; ∀c.P; ∀c.P; ∀c.P; ∀c.P; P; ∀c.P; P; ∀c.P; P; P; P; ∀c.P; ∀c.P; P; ∀c.P; ∀c.P; ∀c.P; P; ∀c.P; ∀c.P; ∀c.P; ∀c.P; ∀c.P; id; ∀c.P; ∀c.P; ♮; ∀c.P; ∀c.P; BCC∀; a, c; b, c; a, c; a; b, c; b; a; b]

[figure: c^{′∗}f^{∗}∀_{c}P; f^{′∗}c^{∗}∀_{c}P; f^{′∗}c^{∗}∀_{c}P; c^{∗}∀_{c}P; c^{′∗}f^{∗}∀_{c}P; f^{′∗}P; f^{′∗}c^{∗}∀_{c}P; f^{′∗}P; c^{∗}∀_{c}P; P; f^{′∗}P; P; c^{′∗}f^{∗}∀_{c}P; f^{∗}∀_{c}P; f^{′∗}P; ∀_{c′}f^{′∗}P; c^{∗}∀_{c}P; ∀_{c}P; P; ∀_{c}P; f^{∗}∀_{c}P; ∀_{c}P; ∀_{c}P; ∀_{c}P; id; f^{∗}∀_{c}P; ∀_{c′}f^{′∗}P; ♮; f^{∗}∀_{c}P; ∀_{c′}f^{′∗}P; BCC∀; A × C; B × C; f′; A × C; A; c′; B × C; B; c; A; B; f]

BCC for ‘exists’

[figure: P; P; P; ∃c.P; P; ∃c.P; P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; P; ∃c.P; P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; id; ∃c.P; ∃c.P; ♮; ∃c.P; ∃c.P; BCC∃; a, c; b, c; a, c; a; b, c; b; a; b]

[figure: f^{′∗}P; P; f^{′∗}P; c^{′∗}f^{∗}∃_{c}P; f^{′∗}P; f^{′∗}c^{∗}∃_{c}P; P; c^{∗}∃_{c}P; c^{′∗}f^{∗}∃_{c}P; f^{′∗}c^{∗}∃_{c}P; f^{′∗}c^{∗}∃_{c}P; c^{∗}∃_{c}P; f^{′∗}P; ∃_{c′}f^{′∗}P; P; ∃_{c}P; c^{′∗}f^{∗}∃_{c}P; f^{∗}∃_{c}P; c^{∗}∃_{c}P; ∃_{c}P; f^{∗}∃_{c}P; ∃_{c}P; ∃_{c}P; ∃_{c}P; id; ∃_{c′}f^{′∗}P; f^{∗}∃_{c}P; ♮; ∃_{c′}f^{′∗}P; f^{∗}∃_{c}P; BCC∃; A × C; B × C; f′; A × C; A; c′; B × C; B; c; A; B; f]

BCC for equality

[figure: P; P; P; c=c′&P; P; c=c′&P; P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; P; c=c′&P; P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; id; c=c′&P; c=c′&P; ♮; c=c′&P; c=c′&P; BCC∃; a, c; b, c; a, c; a, c, c′; b, c; b, c, c′; a, c, c′; b, c, c′]

[figure: f^{′∗}P; P; f^{′∗}P; c^{′∗}f^{∗}Eq_{c}P; f^{′∗}P; f^{′∗}c^{∗}Eq_{c}P; P; c^{∗}Eq_{c}P; c^{′∗}f^{∗}Eq_{c}P; f^{′∗}c^{∗}Eq_{c}P; f^{′∗}c^{∗}Eq_{c}P; c^{∗}Eq_{c}P; f^{′∗}P; Eq_{c′}f^{′∗}P; P; Eq_{c}P; c^{′∗}f^{∗}Eq_{c}P; f^{∗}Eq_{c}P; c^{∗}Eq_{c}P; Eq_{c}P; f^{∗}Eq_{c}P; Eq_{c}P; Eq_{c}P; Eq_{c}P; id; Eq_{c′}f^{′∗}P; f^{∗}Eq_{c}P; ♮; Eq_{c′}f^{′∗}P; f^{∗}Eq_{c}P; BCC=; A × C; B × C; f′; A × C; A × C × C; c′; B × C; B × C × C; c; A × C × C; B × C × C; f]

Frobenius for ‘exists’

[figure: P; ∃c.P; P &Q; P; ∃c.(P &Q); ∃c.P; (∃c.P)&Q; ∃c.P; Q; Q; P &Q; Q; ∃c.(P &Q); Q; (∃c.P)&Q; Q; P &Q; ∃c.(P &Q); ∃c.(P &Q); (∃c.P)&Q; ♮; ∃c.(P &Q); (∃c.P)&Q; Frob∃; b, c; b]

[figure: P; ∃_{c}P; P &c^{∗}Q; P; ∃_{c}(P &c^{∗}Q); ∃_{c}P; (∃_{c}P)&Q; ∃_{c}P; c^{∗}Q; Q; P &c^{∗}Q; c^{∗}Q; ∃_{c}(P &c^{∗}Q); Q; (∃_{c}P)&Q; Q; P &c^{∗}Q; ∃_{c}(P &c^{∗}Q); ∃_{c}(P &c^{∗}Q); (∃_{c}P)&Q; ♮; ∃_{c}(P &c^{∗}Q); (∃_{c}P)&Q; Frob∃; B × C; B; c]

Frobenius for equality

[figure: P; c=c′&P; P &Q; P; c=c′&(P &Q); c=c′&P; (c=c′&P)&Q; c=c′&P; Q; Q; P &Q; Q; c=c′&(P &Q); Q; (c=c′&P)&Q; Q; P &Q; c=c′&(P &Q); c=c′&(P &Q); (c=c′&P)&Q; ♮; c=c′&(P &Q); (c=c′&P)&Q; Frob=; b, c; b, c, c′]

[figure: P; Eq_{c}P; P &c^{∗}Q; P; Eq_{c}(P &c^{∗}Q); Eq_{c}P; (Eq_{c}P)&Q; Eq_{c}P; c^{∗}Q; Q; P &c^{∗}Q; c^{∗}Q; Eq_{c}(P &c^{∗}Q); Q; (Eq_{c}P)&Q; Q; P &c^{∗}Q; Eq_{c}(P &c^{∗}Q); Eq_{c}(P &c^{∗}Q); (Eq_{c}P)&Q; ♮; Eq_{c}(P &c^{∗}Q); (Eq_{c}P)&Q; Frob=; B × C; B × C × C; c]

BCC, categorically This is how the Beck-Chevalley condition (for dependent sums; there is also a variation for dependent products, that we will see soon) is usually stated:

“If the square formed by f, g, f′, g′ in the base category in the diagram below is a pullback, and if P is an object over C, then the natural map from ∑_{f′} g^{′∗}P to g^{∗} ∑_{f} P is an isomorphism.”

The upper part of the diagram below shows how to build the map ♮ : ∑_{f′} g^{′∗}P → g^{∗} ∑_{f} P.

But what does that mean?

[figure: g^{′∗}P; ∑_{f′} g^{′∗}P; g^{′∗}P; g^{′∗}f^{∗} ∑_{f} P; g^{′∗}P; h^{∗} ∑_{f} P; g^{′∗}P; f^{′∗}g^{∗} ∑_{f} P; ∑_{f′} g^{′∗}P; g^{∗} ∑_{f} P; ♮; g^{′∗}f^{∗} ∑_{f} P; h^{∗} ∑_{f} P; h^{∗} ∑_{f} P; f^{′∗}g^{∗} ∑_{f} P; f^{′∗}g^{∗} ∑_{f} P; g^{∗} ∑_{f} P; g^{′∗}P; P; g^{′∗}f^{∗} ∑_{f} P; f^{∗} ∑_{f} P; h^{∗} ∑_{f} P; ∑_{f} P; g^{∗} ∑_{f} P; ∑_{f} P; P; ∑_{f} P; P; f^{∗} ∑_{f} P; ∑_{f} P; ∑_{f} P; id; f^{∗} ∑_{f} P; ∑_{f} P; A ×_{B} C; A ×_{B} C; A ×_{B} C; A ×_{B} C; A ×_{B} C; A; f′; A ×_{B} C; C; g′; A ×_{B} C; B; h; A; B; g; C; B; f]

BCC in a hyperdoctrine In the case of a hyperdoctrine that means that from an object { b, c || P } and a map a ↦ b there are two ways to build an object that deserves the name “{ a || ∃c.P }”...

...and without BCC we would know a map between them going in one direction, ♮ : { a || ∃c.P } → { a || ∃c.P }′, but we wouldn’t know that it is an iso.

[figure: (\begin{matrix}P \\ a, c \end{matrix}); (\begin{matrix}∃c.P \\ a \end{matrix} ); (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}; (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′}; (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′′}; (\begin{matrix}∃c.P \\ a \end{matrix} ); _{(\begin{matrix}∃c.P \\ a \end{matrix} )}_{′}; ♮; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′′}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′′}; _{(\begin{matrix}∃c.P \\ a \end{matrix} )}_{′}; (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}P \\ b, c \end{matrix})}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}_{′}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}∃c.P \\ a \end{matrix} )}_{′}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}P \\ b, c \end{matrix})}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}P \\ b, c \end{matrix})}; _{(\begin{matrix}∃c.P \\ b, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; id; _{(\begin{matrix}∃c.P \\ b, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; a, c; a, c; a, c; a, c; a, c; a; a, c; b, c; a, c; b; a; b; b, c; b]

BCC: collapsing isomorphic objects One trick to make the previous (big) diagram simpler to draw is to draw the objects that are isomorphic and “deserve the same name” — but that may be different — as a single object; these collapsed objects (here just { a, c || ∃c.P }) have more than one functor arrow pointing to them, which indicates that they have more than one construction.

[figure: (\begin{matrix}P \\ a, c \end{matrix}); (\begin{matrix}∃c.P \\ a \end{matrix} ); (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}; (\begin{matrix}∃c.P \\ a \end{matrix} ); _{(\begin{matrix}∃c.P \\ a \end{matrix} )}_{′}; ♮; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ a \end{matrix} )}_{′}; (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}P \\ b, c \end{matrix})}; _{(\begin{matrix}∃c.P \\ a, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ a \end{matrix} )}_{′}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}P \\ b, c \end{matrix})}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}P \\ b, c \end{matrix})}; _{(\begin{matrix}∃c.P \\ b, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; id; _{(\begin{matrix}∃c.P \\ b, c \end{matrix} )}; _{(\begin{matrix}∃c.P \\ b \end{matrix} )}; a, c; a; a, c; b, c; a; b; b, c; b]

BCC for dependent sums: full diagram BCC: full diagram (no isos hidden), in Set^{→}.

[figure: (\begin{matrix}d \\ a, c \end{matrix}); (\begin{matrix}c, d \\ a \end{matrix}); (\begin{matrix}d \\ a, c \end{matrix}); _{(\begin{matrix}c, d \\ a, c \end{matrix})}; (\begin{matrix}d \\ a, c \end{matrix}); _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′}; (\begin{matrix}d \\ a, c \end{matrix}); _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′′}; (\begin{matrix}c, d \\ a \end{matrix}); _{(\begin{matrix}c, d \\ a \end{matrix})}_{′}; ♮; _{(\begin{matrix}c, d \\ a, c \end{matrix})}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′′}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′′}; _{(\begin{matrix}c, d \\ a \end{matrix})}_{′}; (\begin{matrix}d \\ a, c \end{matrix}); _{(\begin{matrix}d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}; _{(\begin{matrix}c, d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}_{′}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}c, d \\ a \end{matrix})}_{′}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; id; _{(\begin{matrix}c, d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; a, c; a, c; a, c; a, c; a, c; a; a, c; b, c; a, c; b; a; b; b, c; b]

BCC: smaller diagram BCC: smaller diagram.

[figure: (\begin{matrix}d \\ a, c \end{matrix}); (\begin{matrix}c, d \\ a \end{matrix}); (\begin{matrix}d \\ a, c \end{matrix}); _{(\begin{matrix}c, d \\ a, c \end{matrix})}; (\begin{matrix}c, d \\ a \end{matrix}); _{(\begin{matrix}c, d \\ a \end{matrix})}; ♮; _{(\begin{matrix}c, d \\ a, c \end{matrix})}; _{(\begin{matrix}c, d \\ a \end{matrix})}; (\begin{matrix}d \\ a, c \end{matrix}); _{(\begin{matrix}d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ a, c \end{matrix})}; _{(\begin{matrix}c, d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ a \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; id; _{(\begin{matrix}c, d \\ b, c \end{matrix})}; _{(\begin{matrix}c, d \\ b \end{matrix})}; a, c; a; a, c; b, c; a; b; b, c; b]

BCC: smaller diagrams BCC: smaller diagrams.

[figure: d; c, d; d; c, d; c, d; c, d; ♮; c, d; c, d; d; d; c, d; c, d; c, d; c, d; d; c, d; d; c, d; c, d; c, d; id; c, d; c, d; a, c; a; a, c; b, c; a; b; b, c; b] \begin{matrix}a ⊢ b & {b, c ⊢ D \atop b ⊢ Σc.D} ; b; p ⊢ p ; b, c; d ⊢ ⟨c, d⟩ \\ a, c; d ⊢ ⟨c, d⟩ \end{matrix} ; a; p ⊢ ⟨c, d⟩[c, d := p]

[figure: c ↦ d; c ↦ d; c ↦ d; d; c ↦ d; c ↦ d; ♮; d; c ↦ d; c ↦ d; c ↦ d; d; d; c ↦ d; c ↦ d; c ↦ d; c ↦ d; c ↦ d; d; c ↦ d; c ↦ d; id; d; c ↦ d; a, c; a; a, c; b, c; a; b; b, c; b] \begin{matrix}a ⊢ b & {b, c ⊢ D \atop b ⊢ Πc.D} ; b; f ⊢ f ; b, c; f ⊢ fc \\ a, c; f ⊢ fc \end{matrix} ; a; f ⊢ λc.fc

BCC: trees

[figure: d; (c=c′), d; d; (c=c), d; (c=c′), d; (c=c′), d; ♮; (c=c), d; (c=c′), d; d; d; (c=c), d; (c=c), d; (c=c′), d; (c=c′), d; d; (c=c′), d; d; (c=c), d; (c=c′), d; (c=c′), d; id; (c=c), d; (c=c′), d; a, c; a, c, c′; a, c; b, c; a, c, c′; b, c, c′; b, c; b, c, c′]  \begin{matrix}a, c ⊢ b, c & {b, c ⊢ D \atop b, c, c′ ⊢ Σ(c=c′).D} ; b, c, c′; ((c=c′), d) ⊢ ((c=c′).d) ; b, c; d ⊢ ⟨(c=c), d⟩ \\ a, c; d ⊢ ⟨(c=c), d⟩ \end{matrix} ; a, c; ((c=c′), d) ⊢ ⟨(c=c′), d⟩