---

Step * 2 of Lemma equipollent-product-sum


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])))
BY
{ D -1 }

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

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [C]  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  Type
4.  b  :  f:a:A  {}\mrightarrow{}  B[a]  \mtimes{}  (x:A  {}\mrightarrow{}  C[x;f  x])
\mvdash{}  \mexists{}a:x:A  {}\mrightarrow{}  (y:B[x]  \mtimes{}  C[x;y]).  (<\mlambda{}x.(fst((a  x))),  \mlambda{}x.(snd((a  x)))>  =  b)


By

---

Latex:
D  -1

---

Home Index