---

Step * 2 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. z : Functor(A;FUN(B;C))
8. T : nat-trans(A;FUN(B;C);f;g)
9. g1 : nat-trans(A;FUN(B;C);g;z)
10. A1 : cat-ob(A)
11. A2 : cat-ob(B)
12. B1 : cat-ob(A)
13. B2 : cat-ob(B)
14. g3 : cat-arrow(A) A1 B1
15. 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))
BY
{ (RenameVar `a1' 10
   THEN RenameVar `a2' 12
   THEN RenameVar `b1' 11
   THEN RenameVar `b2' 13
   THEN RenameVar `xa' (-2)
   THEN RenameVar `xb' (-1)) }

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. z : Functor(A;FUN(B;C))
8. T : nat-trans(A;FUN(B;C);f;g)
9. g1 : nat-trans(A;FUN(B;C);g;z)
10. a1 : cat-ob(A)
11. b1 : cat-ob(B)
12. a2 : cat-ob(A)
13. b2 : cat-ob(B)
14. xa : cat-arrow(A) a1 a2
15. xb : cat-arrow(B) b1 b2
⊢ (cat-comp(C) (f a1 b1) (z a1 b2) (z a2 b2) 
   (cat-comp(C) (f a1 b1) (g a1 b2) (z a1 b2) (cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (T a1 b2)) 
    (g1 a1 b2)) 
   (z a1 a2 xa b2))
= (cat-comp(C) (f a1 b1) (g a2 b2) (z a2 b2) 
   (cat-comp(C) (f a1 b1) (f a2 b2) (g a2 b2) 
    (cat-comp(C) (f a1 b1) (f a1 b2) (f a2 b2) (f a1 b1 b2 xb) (f a1 a2 xa b2)) 
    (T a2 b2)) 
   (g1 a2 b2))
∈ (cat-arrow(C) (f a1 b1) (z a2 b2))

---

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.  z  :  Functor(A;FUN(B;C))
8.  T  :  nat-trans(A;FUN(B;C);f;g)
9.  g1  :  nat-trans(A;FUN(B;C);g;z)
10.  A1  :  cat-ob(A)
11.  A2  :  cat-ob(B)
12.  B1  :  cat-ob(A)
13.  B2  :  cat-ob(B)
14.  g3  :  cat-arrow(A)  A1  B1
15.  g4  :  cat-arrow(B)  A2  B2
\mvdash{}  (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))


By

---

Latex:
(RenameVar  `a1'  10
  THEN  RenameVar  `a2'  12
  THEN  RenameVar  `b1'  11
  THEN  RenameVar  `b2'  13
  THEN  RenameVar  `xa'  (-2)
  THEN  RenameVar  `xb'  (-1))

---

Home Index