---

Step * 1 of Lemma trans-exchange


1. C : SmallCategory
2. D : SmallCategory
3. E : SmallCategory
4. F : Functor(C;D)
5. G : Functor(C;D)
6. H : Functor(C;D)
7. I : Functor(D;E)
8. J : Functor(D;E)
9. K : Functor(D;E)
10. tFG : nat-trans(C;D;F;G)
11. tGH : nat-trans(C;D;G;H)
12. tIJ : nat-trans(D;E;I;J)
13. tJK : nat-trans(D;E;J;K)
14. A : cat-ob(C)
⊢ (trans-horizontal-comp(E;F;G;I;J;tFG;tIJ) o trans-horizontal-comp(E;G;H;J;K;tGH;tJK) A)
= (trans-horizontal-comp(E;F;H;I;K;tFG o tGH;tIJ o tJK) A)
∈ (cat-arrow(E) (functor-comp(F;I) A) (functor-comp(H;K) A))
BY
{ (RepUR ``trans-horizontal-comp trans-comp`` 0 THEN RepUR ``functor-comp`` 0 THEN RW  CatNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  D  :  SmallCategory
3.  E  :  SmallCategory
4.  F  :  Functor(C;D)
5.  G  :  Functor(C;D)
6.  H  :  Functor(C;D)
7.  I  :  Functor(D;E)
8.  J  :  Functor(D;E)
9.  K  :  Functor(D;E)
10.  tFG  :  nat-trans(C;D;F;G)
11.  tGH  :  nat-trans(C;D;G;H)
12.  tIJ  :  nat-trans(D;E;I;J)
13.  tJK  :  nat-trans(D;E;J;K)
14.  A  :  cat-ob(C)
\mvdash{}  (trans-horizontal-comp(E;F;G;I;J;tFG;tIJ)  o  trans-horizontal-comp(E;G;H;J;K;tGH;tJK)  A)
=  (trans-horizontal-comp(E;F;H;I;K;tFG  o  tGH;tIJ  o  tJK)  A)


By

---

Latex:
(RepUR  ``trans-horizontal-comp  trans-comp``  0
  THEN  RepUR  ``functor-comp``  0
  THEN  RW    CatNormC  0
  THEN  Auto)

---

Home Index