---

Step * of Lemma equipollent-product-sum

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:a:A ⟶ B[a] ⟶ Type].  x:A ⟶ (y:B[x] × C[x;y]) ~ f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])
BY
{ (Auto
   THEN (With ⌜λF.<λx.(fst((F x))), λx.(snd((F x)))>⌝ (D 0)⋅ THENA Auto)
   THEN D 0
   THEN RepUR ``inject surject`` 0
   THEN Auto) }

1
1. A : Type
2. B : A ⟶ Type
3. C : a:A ⟶ B[a] ⟶ Type
4. a1 : x:A ⟶ (y:B[x] × C[x;y])
5. a2 : x:A ⟶ (y:B[x] × C[x;y])
6. <λx.(fst((a1 x))), λx.(snd((a1 x)))> = <λx.(fst((a2 x))), λx.(snd((a2 x)))> ∈ (f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x]))
⊢ a1 = a2 ∈ (x:A ⟶ (y:B[x] × C[x;y]))

2
1. [A] : Type
2. [B] : A ⟶ Type
3. [C] : a:A ⟶ B[a] ⟶ Type
4. b : f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])
⊢ ∃a:x:A ⟶ (y:B[x] × C[x;y]). (<λx.(fst((a x))), λx.(snd((a x)))> = b ∈ (f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  Type].
    x:A  {}\mrightarrow{}  (y:B[x]  \mtimes{}  C[x;y])  \msim{}  f:a:A  {}\mrightarrow{}  B[a]  \mtimes{}  (x:A  {}\mrightarrow{}  C[x;f  x])


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}\mlambda{}F.<\mlambda{}x.(fst((F  x))),  \mlambda{}x.(snd((F  x)))>\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  RepUR  ``inject  surject``  0
  THEN  Auto)

---

Home Index