---

Step * 1 1 1 of Lemma functor-uncurry_wf


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))
BY
{ (RenameVar `a1' 7
   THEN RenameVar `a2' 9
   THEN RenameVar `b1' 8
   THEN RenameVar `b2' 10
   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))
5. g : Functor(A;FUN(B;C))
6. T : nat-trans(A;FUN(B;C);f;g)
7. a1 : cat-ob(A)
8. b1 : cat-ob(B)
9. a2 : cat-ob(A)
10. b2 : cat-ob(B)
11. xa : cat-arrow(A) a1 a2
12. xb : cat-arrow(B) b1 b2
⊢ (cat-comp(C) (f a1 b1) (g a1 b2) (g a2 b2) (cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (T a1 b2)) 
   (g a1 a2 xa 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))
∈ (cat-arrow(C) (f a1 b1) (g a2 b2))

---

Latex:

---

Latex:

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
\mvdash{}  (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))


By

---

Latex:
(RenameVar  `a1'  7
  THEN  RenameVar  `a2'  9
  THEN  RenameVar  `b1'  8
  THEN  RenameVar  `b2'  10
  THEN  RenameVar  `xa'  (-2)
  THEN  RenameVar  `xb'  (-1))

---

Home Index