---

Step * of Lemma nat-trans-assoc-comp-equation

∀[C,D:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[t1:nat-trans(C;D;F;H)]. ∀[t2:nat-trans(C;D;H;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) 
     (cat-comp(D) (ob(F) B) (ob(H) B) (ob(G) B) (t1 B) (t2 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)) 
     (cat-comp(D) (ob(F) B') (ob(H) B') (ob(G) B') (t1 B') (t2 B')))
  ∈ (cat-arrow(D) (ob(F) A) (ob(G) B')))
BY
{ (Intros
   THEN (Assert (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) (t1 o t2 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)) 
                  (t1 o t2 B'))
               ∈ (cat-arrow(D) (ob(F) A) (ob(G) B')) BY
               Auto)
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F,G,H:Functor(C;D)].  \mforall{}[t1:nat-trans(C;D;F;H)].  \mforall{}[t2:nat-trans(C;D;H;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) 
          (cat-comp(D)  (ob(F)  B)  (ob(H)  B)  (ob(G)  B)  (t1  B)  (t2  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)) 
          (cat-comp(D)  (ob(F)  B')  (ob(H)  B')  (ob(G)  B')  (t1  B')  (t2  B'))))


By

---

Latex:
(Intros
  THEN  (Assert  (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)  (t1  o  t2  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)) 
                                (t1  o  t2  B'))  BY
                          Auto)
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index