---

Step * 1 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)
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])
BY
{ ((D -3 THEN D -2) THEN All Reduce THEN (SplitPair (-1) THENA 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. a : A
11. a3 : C[a]
12. a4 : A
13. a5 : C[a4]
14. (f a) = (f a4) ∈ B
15. (g a a3) = (g a4 a5) ∈ D[f a]
⊢ <a, a3> = <a4, a5> ∈ (a:A × C[a])

---

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)
10.  a1  :  a:A  \mtimes{}  C[a]
11.  a2  :  a:A  \mtimes{}  C[a]
12.  let  a,c  =  a1  in  <f  a,  g  a  c>  =  let  a,c  =  a2  in  <f  a,  g  a  c>
\mvdash{}  a1  =  a2


By

---

Latex:
((D  -3  THEN  D  -2)  THEN  All  Reduce  THEN  (SplitPair  (-1)  THENA  Auto))

---

Home Index