---

Step * 2 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. h : Functor(A;FUN(B;C))
7. t1 : nat-trans(A;FUN(B;C);f;g)
8. t2 : nat-trans(A;FUN(B;C);g;h)
9. a1 : cat-ob(A)
10. b1 : cat-ob(B)
11. a2 : cat-ob(A)
12. b2 : cat-ob(B)
13. xa : cat-arrow(A) a1 a2
14. xb : cat-arrow(B) b1 b2
⊢ (cat-comp(C) (f a1 b1) (h a1 b2) (h a2 b2) 
   (cat-comp(C) (f a1 b1) (g a1 b2) (h a1 b2) (cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (t1 a1 b2)) 
    (t2 a1 b2)) 
   (h a1 a2 xa b2))
= (cat-comp(C) (f a1 b1) (g a2 b2) (h 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)) 
    (t1 a2 b2)) 
   (t2 a2 b2))
∈ (cat-arrow(C) (f a1 b1) (h a2 b2))
BY
{ ((InstLemma `nat-trans-equation` [⌜A⌝;⌜FUN(B;C)⌝;⌜f⌝;⌜h⌝;⌜t1 o t2⌝;⌜a1⌝;⌜a2⌝;⌜xa⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN (MemTypeHD (-1) THENA Auto)) }

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. h : Functor(A;FUN(B;C))
7. t1 : nat-trans(A;FUN(B;C);f;g)
8. t2 : nat-trans(A;FUN(B;C);g;h)
9. a1 : cat-ob(A)
10. b1 : cat-ob(B)
11. a2 : cat-ob(A)
12. b2 : cat-ob(B)
13. xa : cat-arrow(A) a1 a2
14. xb : cat-arrow(B) b1 b2
15. t1 a1 o t2 a1 o h a1 a2 xa = f a1 a2 xa o t1 a2 o t2 a2 ∈ (A:cat-ob(B) ⟶ (cat-arrow(C) (f a1 A) (h a2 A)))
16. ∀A,B@0:cat-ob(B). ∀g@0:cat-arrow(B) A B@0.
      ((cat-comp(C) (f a1 A) (h a2 A) (h a2 B@0) (t1 a1 o t2 a1 o h a1 a2 xa A) (h a2 A B@0 g@0))
      = (cat-comp(C) (f a1 A) (f a1 B@0) (h a2 B@0) (f a1 A B@0 g@0) (t1 a1 o t2 a1 o h a1 a2 xa B@0))
      ∈ (cat-arrow(C) (f a1 A) (h a2 B@0)))
⊢ (cat-comp(C) (f a1 b1) (h a1 b2) (h a2 b2) 
   (cat-comp(C) (f a1 b1) (g a1 b2) (h a1 b2) (cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (t1 a1 b2)) 
    (t2 a1 b2)) 
   (h a1 a2 xa b2))
= (cat-comp(C) (f a1 b1) (g a2 b2) (h 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)) 
    (t1 a2 b2)) 
   (t2 a2 b2))
∈ (cat-arrow(C) (f a1 b1) (h 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.  h  :  Functor(A;FUN(B;C))
7.  t1  :  nat-trans(A;FUN(B;C);f;g)
8.  t2  :  nat-trans(A;FUN(B;C);g;h)
9.  a1  :  cat-ob(A)
10.  b1  :  cat-ob(B)
11.  a2  :  cat-ob(A)
12.  b2  :  cat-ob(B)
13.  xa  :  cat-arrow(A)  a1  a2
14.  xb  :  cat-arrow(B)  b1  b2
\mvdash{}  (cat-comp(C)  (f  a1  b1)  (h  a1  b2)  (h  a2  b2) 
      (cat-comp(C)  (f  a1  b1)  (g  a1  b2)  (h  a1  b2) 
        (cat-comp(C)  (f  a1  b1)  (f  a1  b2)  (g  a1  b2)  (f  a1  b1  b2  xb)  (t1  a1  b2)) 
        (t2  a1  b2)) 
      (h  a1  a2  xa  b2))
=  (cat-comp(C)  (f  a1  b1)  (g  a2  b2)  (h  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)) 
        (t1  a2  b2)) 
      (t2  a2  b2))


By

---

Latex:
((InstLemma  `nat-trans-equation`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}FUN(B;C)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}t1  o  t2\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}xa\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  (MemTypeHD  (-1)  THENA  Auto))

---

Home Index