---

Step * of Lemma equipollent-union-sum

∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].
  a:A × C[a] + (b:B × D[b]) ~ d:A + B × case d of inl(a) => C[a] | inr(b) => D[b]
BY
{ (Auto
   THEN (With ⌜λd.case d of inl(p) => let a,c = p in <inl a, c> | inr(p) => let b,d = p in <inr b , d>⌝ (D 0)⋅
         THENA Auto
         )
   THEN D 0
   THEN RepUR ``inject surject`` 0
   THEN Auto) }

1
1. A : Type
2. B : Type
3. C : A ⟶ Type
4. D : B ⟶ Type
5. a1 : a:A × C[a] + (b:B × D[b])@i
6. a2 : a:A × C[a] + (b:B × D[b])@i
7. case a1 of inl(p) => let a,c = p in <inl a, c> | inr(p) => let b,d = p in <inr b , d>
= case a2 of inl(p) => let a,c = p in <inl a, c> | inr(p) => let b,d = p in <inr b , d>
∈ (d:A + B × case d of inl(a) => C[a] | inr(b) => D[b])
⊢ a1 = a2 ∈ (a:A × C[a] + (b:B × D[b]))

2
1. [A] : Type
2. [B] : Type
3. [C] : A ⟶ Type
4. [D] : B ⟶ Type
5. b : d:A + B × case d of inl(a) => C[a] | inr(b) => D[b]@i
⊢ ∃a:a:A × C[a] + (b:B × D[b])
   (case a of inl(p) => let a,c = p in <inl a, c> | inr(p) => let b,d = p in <inr b , d>
   = b
   ∈ (d:A + B × case d of inl(a) => C[a] | inr(b) => D[b]))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  Type].  \mforall{}[D:B  {}\mrightarrow{}  Type].
    a:A  \mtimes{}  C[a]  +  (b:B  \mtimes{}  D[b])  \msim{}  d:A  +  B  \mtimes{}  case  d  of  inl(a)  =>  C[a]  |  inr(b)  =>  D[b]


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}\mlambda{}d.case  d
                                  of  inl(p)  =>
                                  let  a,c  =  p 
                                  in  <inl  a,  c>
                                  |  inr(p)  =>
                                  let  b,d  =  p 
                                  in  <inr  b  ,  d>\mkleeneclose{}  (D  0)\mcdot{}
              THENA  Auto
              )
  THEN  D  0
  THEN  RepUR  ``inject  surject``  0
  THEN  Auto)

---

Home Index