---

Step * of Lemma trans-exchange

∀[C,D,E:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[I,J,K:Functor(D;E)]. ∀[tFG:nat-trans(C;D;F;G)].
∀[tGH:nat-trans(C;D;G;H)]. ∀[tIJ:nat-trans(D;E;I;J)]. ∀[tJK:nat-trans(D;E;J;K)].
  (trans-horizontal-comp(E;F;G;I;J;tFG;tIJ) o trans-horizontal-comp(E;G;H;J;K;tGH;tJK)
  = trans-horizontal-comp(E;F;H;I;K;tFG o tGH;tIJ o tJK)
  ∈ nat-trans(C;E;functor-comp(F;I);functor-comp(H;K)))
BY
{ (Intros THEN (BLemma `nat-trans-equal2` THENA Auto) THEN (FunExt THENA Auto)) }

1
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) (ob(functor-comp(F;I)) A) (ob(functor-comp(H;K)) A))

---

Latex:

---

Latex:
\mforall{}[C,D,E:SmallCategory].  \mforall{}[F,G,H:Functor(C;D)].  \mforall{}[I,J,K:Functor(D;E)].  \mforall{}[tFG:nat-trans(C;D;F;G)].
\mforall{}[tGH:nat-trans(C;D;G;H)].  \mforall{}[tIJ:nat-trans(D;E;I;J)].  \mforall{}[tJK:nat-trans(D;E;J;K)].
    (trans-horizontal-comp(E;F;G;I;J;tFG;tIJ)  o  trans-horizontal-comp(E;G;H;J;K;tGH;tJK)
    =  trans-horizontal-comp(E;F;H;I;K;tFG  o  tGH;tIJ  o  tJK))


By

---

Latex:
(Intros  THEN  (BLemma  `nat-trans-equal2`  THENA  Auto)  THEN  (FunExt  THENA  Auto))

---

Home Index