---

Step * of Lemma nat-trans-comp-equation

No Annotations
∀[C,D:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[t1:nat-trans(C;D;F;G)]. ∀[t2:nat-trans(C;D;G;H)]. ∀[A,B:cat-ob(C)].
∀[g:cat-arrow(C) A B].
  ((cat-comp(D) (F A) (H A) (H B) (cat-comp(D) (F A) (G A) (H A) (t1 A) (t2 A)) (H A B g))
  = (cat-comp(D) (F A) (F B) (H B) (F A B g) (cat-comp(D) (F B) (G B) (H B) (t1 B) (t2 B)))
  ∈ (cat-arrow(D) (F A) (H B)))
BY
{ (Intros
   THEN (Assert (cat-comp(D) (F A) (H A) (H B) (t1 o t2 A) (H A B g))
               = (cat-comp(D) (F A) (F B) (H B) (F A B g) (t1 o t2 B))
               ∈ (cat-arrow(D) (F A) (H B)) BY
               (BLemma `nat-trans-equation` THEN Auto))
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (Assert  (cat-comp(D)  (F  A)  (H  A)  (H  B)  (t1  o  t2  A)  (H  A  B  g))
                          =  (cat-comp(D)  (F  A)  (F  B)  (H  B)  (F  A  B  g)  (t1  o  t2  B))  BY
                          (BLemma  `nat-trans-equation`  THEN  Auto))
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index