---

Step * of Lemma nat-trans-equation

∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[T:nat-trans(C;D;F;G)]. ∀[A,B:cat-ob(C)]. ∀[g:cat-arrow(C) A B].
  ((cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(G) B) (T A) (functor-arrow(G) A B g))
  = (cat-comp(D) (functor-ob(F) A) (functor-ob(F) B) (functor-ob(G) B) (functor-arrow(F) A B g) (T B))
  ∈ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) B)))
BY
{ ((Auto THEN DVar `T'⋅) THEN BackThruSomeHyp) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  DVar  `T'\mcdot{})  THEN  BackThruSomeHyp)

---

Home Index