---

Step * of Lemma nat-trans-comp-equation2

No Annotations
∀[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) (J (F A)) (J (G B)) v 
    (cat-comp(E) (J (F A)) (J (G A)) (J (G B)) (J (F A) (G A) (tFG A)) (J (G A) (G B) (G A B g))))
  = (cat-comp(E) (J (F A)) (J (G B)) v 
     (cat-comp(E) (J (F A)) (J (F B)) (J (G B)) (J (F A) (F B) (F A B g)) (J (F B) (G B) (tFG B))))
  ∈ ((cat-arrow(E) (J (G B)) v) ⟶ (cat-arrow(E) (J (F A)) v)))
BY
{ ((Intros THEN Unhide) THEN (RWO "functor-arrow-comp<" 0 THENA Auto) THEN RWO "nat-trans-equation" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\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)  (J  (F  A))  (J  (G  B))  v 
        (cat-comp(E)  (J  (F  A))  (J  (G  A))  (J  (G  B))  (J  (F  A)  (G  A)  (tFG  A))  (J  (G  A)  (G  B)  (G  A  B  g))))
    =  (cat-comp(E)  (J  (F  A))  (J  (G  B))  v 
          (cat-comp(E)  (J  (F  A))  (J  (F  B))  (J  (G  B))  (J  (F  A)  (F  B)  (F  A  B  g))  (J  (F  B)  (G  B)  (tFG  B)))))


By

---

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

---

Home Index