---

Step * 1 of Lemma product_functionality_wrt_equipollent_dependent


1. [A] : Type
2. [B] : Type
3. [C] : A ⟶ Type
4. [D] : B ⟶ Type
5. f : A ⟶ B
6. Bij(A;B;f)
7. ∀a:A. ∃f@0:C[a] ⟶ D[f a]. Bij(C[a];D[f a];f@0)
8. g : a:A ⟶ C[a] ⟶ D[f a]
9. ∀a:A. Bij(C[a];D[f a];g a)
⊢ ∃f:(a:A × C[a]) ⟶ (b:B × D[b]). Bij(a:A × C[a];b:B × D[b];f)
BY
{ TACTIC:((With ⌜λac.let a,c = ac in <f a, g a c>⌝ (D 0)⋅ THEN Auto) THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))) }

1
1. A : Type
2. B : Type
3. C : A ⟶ Type
4. D : B ⟶ Type
5. f : A ⟶ B
6. Bij(A;B;f)
7. ∀a:A. ∃f@0:C[a] ⟶ D[f a]. Bij(C[a];D[f a];f@0)
8. g : a:A ⟶ C[a] ⟶ D[f a]
9. ∀a:A. Bij(C[a];D[f a];g a)
10. a1 : a:A × C[a]
11. a2 : a:A × C[a]
12. let a,c = a1 in <f a, g a c> = let a,c = a2 in <f a, g a c> ∈ (b:B × D[b])
⊢ a1 = a2 ∈ (a:A × C[a])

2
1. [A] : Type
2. [B] : Type
3. [C] : A ⟶ Type
4. [D] : B ⟶ Type
5. f : A ⟶ B
6. Bij(A;B;f)
7. ∀a:A. ∃f@0:C[a] ⟶ D[f a]. Bij(C[a];D[f a];f@0)
8. g : a:A ⟶ C[a] ⟶ D[f a]
9. ∀a:A. Bij(C[a];D[f a];g a)
10. b : b:B × D[b]
⊢ ∃a:a:A × C[a]. (let a,c = a in <f a, g a c> = b ∈ (b:B × D[b]))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  A  {}\mrightarrow{}  Type
4.  [D]  :  B  {}\mrightarrow{}  Type
5.  f  :  A  {}\mrightarrow{}  B
6.  Bij(A;B;f)
7.  \mforall{}a:A.  \mexists{}f@0:C[a]  {}\mrightarrow{}  D[f  a].  Bij(C[a];D[f  a];f@0)
8.  g  :  a:A  {}\mrightarrow{}  C[a]  {}\mrightarrow{}  D[f  a]
9.  \mforall{}a:A.  Bij(C[a];D[f  a];g  a)
\mvdash{}  \mexists{}f:(a:A  \mtimes{}  C[a])  {}\mrightarrow{}  (b:B  \mtimes{}  D[b]).  Bij(a:A  \mtimes{}  C[a];b:B  \mtimes{}  D[b];f)


By

---

Latex:
TACTIC:((With  \mkleeneopen{}\mlambda{}ac.let  a,c  =  ac  in  <f  a,  g  a  c>\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
                THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto))
                )

---

Home Index