---

Step * of Lemma nat-trans-comp-equation2

∀[C,D,E:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[J:Functor(D;E)]. ∀[tFG:nat-trans(C;D;F;G)]. ∀[A,B:cat-ob(C)].
∀[g:cat-arrow(C) A B]. ∀[v:cat-ob(E)].
  ((cat-comp(E) (ob(J) (ob(F) A)) (ob(J) (ob(G) B)) v 
    (cat-comp(E) (ob(J) (ob(F) A)) (ob(J) (ob(G) A)) (ob(J) (ob(G) B)) (arrow(J) (ob(F) A) (ob(G) A) (tFG A)) 
     (arrow(J) (ob(G) A) (ob(G) B) (arrow(G) A B g))))
  = (cat-comp(E) (ob(J) (ob(F) A)) (ob(J) (ob(G) B)) v 
     (cat-comp(E) (ob(J) (ob(F) A)) (ob(J) (ob(F) B)) (ob(J) (ob(G) B)) (arrow(J) (ob(F) A) (ob(F) B) (arrow(F) A B g)) 
      (arrow(J) (ob(F) B) (ob(G) B) (tFG B))))
  ∈ ((cat-arrow(E) (ob(J) (ob(G) B)) v) ⟶ (cat-arrow(E) (ob(J) (ob(F) A)) v)))
BY
{ (Auto THEN (RWO "functor-arrow-comp<" 0 THENA Auto) THEN RWO "nat-trans-equation" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,D,E:SmallCategory].  \mforall{}[F,G:Functor(C;D)].  \mforall{}[J:Functor(D;E)].  \mforall{}[tFG:nat-trans(C;D;F;G)].
\mforall{}[A,B:cat-ob(C)].  \mforall{}[g:cat-arrow(C)  A  B].  \mforall{}[v:cat-ob(E)].
    ((cat-comp(E)  (ob(J)  (ob(F)  A))  (ob(J)  (ob(G)  B))  v 
        (cat-comp(E)  (ob(J)  (ob(F)  A))  (ob(J)  (ob(G)  A))  (ob(J)  (ob(G)  B)) 
          (arrow(J)  (ob(F)  A)  (ob(G)  A)  (tFG  A)) 
          (arrow(J)  (ob(G)  A)  (ob(G)  B)  (arrow(G)  A  B  g))))
    =  (cat-comp(E)  (ob(J)  (ob(F)  A))  (ob(J)  (ob(G)  B))  v 
          (cat-comp(E)  (ob(J)  (ob(F)  A))  (ob(J)  (ob(F)  B))  (ob(J)  (ob(G)  B)) 
            (arrow(J)  (ob(F)  A)  (ob(F)  B)  (arrow(F)  A  B  g)) 
            (arrow(J)  (ob(F)  B)  (ob(G)  B)  (tFG  B)))))


By

---

Latex:
(Auto  THEN  (RWO  "functor-arrow-comp<"  0  THENA  Auto)  THEN  RWO  "nat-trans-equation"  0  THEN  Auto)

---

Home Index