---

Step * of Lemma functor-uncurry_wf

No Annotations
∀[A,B,C:SmallCategory].  (functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C)))
BY
{ (ProveWfLemma THEN DProds THEN All Reduce) }

1
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. f : Functor(A;FUN(B;C))
5. g : Functor(A;FUN(B;C))
6. T : nat-trans(A;FUN(B;C);f;g)
7. A2 : cat-ob(A)
8. A3 : cat-ob(B)
9. B2 : cat-ob(A)
10. B3 : cat-ob(B)
11. g2 : cat-arrow(A) A2 B2
12. g3 : cat-arrow(B) A3 B3
⊢ (cat-comp(C) (f A2 A3) (g A2 B3) (g B2 B3) (cat-comp(C) (f A2 A3) (f A2 B3) (g A2 B3) (f A2 A3 B3 g3) (T A2 B3)) 
   (g A2 B2 g2 B3))
= (cat-comp(C) (f A2 A3) (f B2 B3) (g B2 B3) 
   (cat-comp(C) (f A2 A3) (f A2 B3) (f B2 B3) (f A2 A3 B3 g3) (f A2 B2 g2 B3)) 
   (T B2 B3))
∈ (cat-arrow(C) (f A2 A3) (g B2 B3))

2
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. f : Functor(A;FUN(B;C))
5. g : Functor(A;FUN(B;C))
6. z : Functor(A;FUN(B;C))
7. T : nat-trans(A;FUN(B;C);f;g)
8. g1 : nat-trans(A;FUN(B;C);g;z)
9. A1 : cat-ob(A)
10. A2 : cat-ob(B)
11. B1 : cat-ob(A)
12. B2 : cat-ob(B)
13. g3 : cat-arrow(A) A1 B1
14. g4 : cat-arrow(B) A2 B2
⊢ (cat-comp(C) (f A1 A2) (z A1 B2) (z B1 B2) 
   (cat-comp(C) (f A1 A2) (g A1 B2) (z A1 B2) (cat-comp(C) (f A1 A2) (f A1 B2) (g A1 B2) (f A1 A2 B2 g4) (T A1 B2)) 
    (g1 A1 B2)) 
   (z A1 B1 g3 B2))
= (cat-comp(C) (f A1 A2) (g B1 B2) (z B1 B2) 
   (cat-comp(C) (f A1 A2) (f B1 B2) (g B1 B2) 
    (cat-comp(C) (f A1 A2) (f A1 B2) (f B1 B2) (f A1 A2 B2 g4) (f A1 B1 g3 B2)) 
    (T B1 B2)) 
   (g1 B1 B2))
∈ (cat-arrow(C) (f A1 A2) (z B1 B2))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B,C:SmallCategory].    (functor-uncurry(C)  \mmember{}  Functor(FUN(A;FUN(B;C));FUN(A  \mtimes{}  B;C)))


By

---

Latex:
(ProveWfLemma  THEN  DProds  THEN  All  Reduce)

---

Home Index