---

Step * of Lemma nat-trans-assoc-equation

No Annotations
∀[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) (F A) (G B) (G B') (cat-comp(D) (F A) (F B) (G B) (F A B g) (T B)) (G B B' h))
  = (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
  ∈ (cat-arrow(D) (F A) (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) THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. C : SmallCategory
2. D : SmallCategory
3. F : Functor(C;D)
4. G : Functor(C;D)
5. T : nat-trans(C;D;F;G)
6. A : cat-ob(C)
7. B : cat-ob(C)
8. B' : cat-ob(C)
9. g : cat-arrow(C) A B
10. h : cat-arrow(C) B B'
11. (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
= (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
∈ (cat-arrow(D) (F A) (G B'))
⊢ (cat-comp(D) (F A) (G B) (G B') (cat-comp(D) (F A) (F B) (G B) (F A B g) (T B)) (G B B' h))
= (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
∈ (cat-arrow(D) (F A) (G B'))

---

Latex:

---

Latex:
No  Annotations
\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)  (F  A)  (G  B)  (G  B')  (cat-comp(D)  (F  A)  (F  B)  (G  B)  (F  A  B  g)  (T  B))  (G  B  B'  h))
    =  (cat-comp(D)  (F  A)  (F  B')  (G  B')  (cat-comp(D)  (F  A)  (F  B)  (F  B')  (F  A  B  g)  (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)  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA)

---

Home Index