---

Step * of Lemma equipollent-product-product

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:a:A ⟶ B[a] ⟶ Type].  x:A ⟶ y:B[x] ⟶ C[x;y] ~ p:(a:A × B[a]) ⟶ C[fst(p);snd(p)]
BY
{ (Auto THEN (With ⌜λF,p. let x,y = p in F x y⌝ (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. (λp.let x,y = p in a1 x y) = (λp.let x,y = p in a2 x y) ∈ (p:(a:A × B[a]) ⟶ C[fst(p);snd(p)])
⊢ 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 : p:(a:A × B[a]) ⟶ C[fst(p);snd(p)]
⊢ ∃a:x:A ⟶ y:B[x] ⟶ C[x;y]. ((λp.let x,y = p in a x y) = b ∈ (p:(a:A × B[a]) ⟶ C[fst(p);snd(p)]))

---

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]  {}\mrightarrow{}  C[x;y]  \msim{}  p:(a:A  \mtimes{}  B[a])  {}\mrightarrow{}  C[fst(p);snd(p)]


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}\mlambda{}F,p.  let  x,y  =  p  in  F  x  y\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  RepUR  ``inject  surject``  0
  THEN  Auto)

---

Home Index