---

Step * 1 of Lemma functor-uncurry_wf


1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. ∀f:Functor(A;FUN(B;C))
     (functor(ob(p) = f (fst(p)) (snd(p));
              arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y))) 
                             (f (fst(x)) (fst(y)) (fst(p)) (snd(x))) 
                             (f (fst(y)) (snd(x)) (snd(y)) (snd(p)))) ∈ Functor(A × B;C))
5. f : Functor(A;FUN(B;C))
6. g : Functor(A;FUN(B;C))
7. T : nat-trans(A;FUN(B;C);f;g)
8. A2 : cat-ob(A)
9. A3 : cat-ob(B)
10. B2 : cat-ob(A)
11. B3 : cat-ob(B)
12. g2 : cat-arrow(A) A2 B2
13. g3 : cat-arrow(B) A3 B3
⊢ (cat-comp(C) (f A2 A3) (g A2 A3) (g B2 B3) (T A2 A3) 
   (cat-comp(C) (g A2 A3) (g B2 A3) (g B2 B3) (g A2 B2 g2 A3) (g B2 A3 B3 g3)))
= (cat-comp(C) (f A2 A3) (f B2 B3) (g B2 B3) 
   (cat-comp(C) (f A2 A3) (f B2 A3) (f B2 B3) (f A2 B2 g2 A3) (f B2 A3 B3 g3)) 
   (T B2 B3))
∈ (cat-arrow(C) (f A2 A3) (g B2 B3))
BY
{ (RW CatNormC 0 THEN Auto) }

1
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. ∀f:Functor(A;FUN(B;C))
     (functor(ob(p) = f (fst(p)) (snd(p));
              arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y))) 
                             (f (fst(x)) (fst(y)) (fst(p)) (snd(x))) 
                             (f (fst(y)) (snd(x)) (snd(y)) (snd(p)))) ∈ Functor(A × B;C))
5. f : Functor(A;FUN(B;C))
6. g : Functor(A;FUN(B;C))
7. T : nat-trans(A;FUN(B;C);f;g)
8. A2 : cat-ob(A)
9. A3 : cat-ob(B)
10. B2 : cat-ob(A)
11. B3 : cat-ob(B)
12. g2 : cat-arrow(A) A2 B2
13. 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))

---

Latex:

---

Latex:

1.  A  :  SmallCategory
2.  B  :  SmallCategory
3.  C  :  SmallCategory
4.  \mforall{}f:Functor(A;FUN(B;C))
          (functor(ob(p)  =  f  (fst(p))  (snd(p));
                            arrow(x,y,p)  =  cat-comp(C)  (f  (fst(x))  (snd(x)))  (f  (fst(y))  (snd(x))) 
                                                          (f  (fst(y))  (snd(y))) 
                                                          (f  (fst(x))  (fst(y))  (fst(p))  (snd(x))) 
                                                          (f  (fst(y))  (snd(x))  (snd(y))  (snd(p))))  \mmember{}  Functor(A  \mtimes{}  B;C))
5.  f  :  Functor(A;FUN(B;C))
6.  g  :  Functor(A;FUN(B;C))
7.  T  :  nat-trans(A;FUN(B;C);f;g)
8.  A2  :  cat-ob(A)
9.  A3  :  cat-ob(B)
10.  B2  :  cat-ob(A)
11.  B3  :  cat-ob(B)
12.  g2  :  cat-arrow(A)  A2  B2
13.  g3  :  cat-arrow(B)  A3  B3
\mvdash{}  (cat-comp(C)  (f  A2  A3)  (g  A2  A3)  (g  B2  B3)  (T  A2  A3) 
      (cat-comp(C)  (g  A2  A3)  (g  B2  A3)  (g  B2  B3)  (g  A2  B2  g2  A3)  (g  B2  A3  B3  g3)))
=  (cat-comp(C)  (f  A2  A3)  (f  B2  B3)  (g  B2  B3) 
      (cat-comp(C)  (f  A2  A3)  (f  B2  A3)  (f  B2  B3)  (f  A2  B2  g2  A3)  (f  B2  A3  B3  g3)) 
      (T  B2  B3))


By

---

Latex:
(RW  CatNormC  0  THEN  Auto)

---

Home Index