---

Step * of Lemma is-nat-trans

No Annotations
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[trans:A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A))].
  trans ∈ nat-trans(C;D;F;G) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
              ((cat-comp(D) (F A) (G A) (G B) (trans A) (G A B g))
              = (cat-comp(D) (F A) (F B) (G B) (F A B g) (trans B))
              ∈ (cat-arrow(D) (F A) (G B)))
BY
{ (Intros THEN Unhide THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C,D:SmallCategory].  \mforall{}[F,G:Functor(C;D)].  \mforall{}[trans:A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(D)  (F  A)  (G  A))].
    trans  \mmember{}  nat-trans(C;D;F;G) 
    supposing  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.
                            ((cat-comp(D)  (F  A)  (G  A)  (G  B)  (trans  A)  (G  A  B  g))
                            =  (cat-comp(D)  (F  A)  (F  B)  (G  B)  (F  A  B  g)  (trans  B)))


By

---

Latex:
(Intros  THEN  Unhide  THEN  MemTypeCD  THEN  Auto)

---

Home Index