---

Step * of Lemma nat-trans-assoc-equation

∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[T:nat-trans(C;D;F;G)]. ∀[A,B,B':cat-ob(C)]. ∀[g:cat-arrow(C) A B].
∀[h:cat-arrow(C) B B'].
  ((cat-comp(D) (ob(F) A) (ob(G) B) (ob(G) B') (cat-comp(D) (ob(F) A) (ob(F) B) (ob(G) B) (arrow(F) A B g) (T B)) 
    (arrow(G) B B' h))
  = (cat-comp(D) (ob(F) A) (ob(F) B') (ob(G) B') 
     (cat-comp(D) (ob(F) A) (ob(F) B) (ob(F) B') (arrow(F) A B g) (arrow(F) B B' h)) 
     (T B'))
  ∈ (cat-arrow(D) (ob(F) A) (ob(G) B')))
BY
{ (Intros
   THEN (InstLemma `nat-trans-equation`[⌜C⌝;⌜D⌝;⌜F⌝;⌜G⌝;⌜T⌝;⌜A⌝;⌜B'⌝;⌜cat-comp(C) A B B' g h⌝]⋅ THENA Auto)
   THEN RW (CatNormC) (-1)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (InstLemma  `nat-trans-equation`[\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B'\mkleeneclose{};\mkleeneopen{}cat-comp(C)  A  B  B'  g  h\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RW  (CatNormC)  (-1)
  THEN  Auto)

---

Home Index