### Nuprl 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)))`

Proof

Definitions occuring in Statement :  trans-horizontal-comp: `trans-horizontal-comp(E;F;G;J;K;tFG;tJK)` functor-comp: `functor-comp(F;G)` trans-comp: `t1 o t2` nat-trans: `nat-trans(C;D;F;G)` cat-functor: `Functor(C1;C2)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` trans-comp: `t1 o t2` trans-horizontal-comp: `trans-horizontal-comp(E;F;G;J;K;tFG;tJK)` all: `∀x:A. B[x]` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` functor-comp: `functor-comp(F;G)` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` nat-trans: `nat-trans(C;D;F;G)` true: `True` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  nat-trans-equal2 functor-comp_wf trans-comp_wf trans-horizontal-comp_wf cat-ob_wf nat-trans_wf cat-functor_wf small-category_wf ap_mk_nat_trans_lemma ob_mk_functor_lemma cat-arrow_wf functor-ob_wf cat-comp_wf functor-arrow_wf equal_wf squash_wf true_wf nat-trans-equation cat-comp-assoc functor-arrow-comp nat-trans-assoc-equation nat-trans-comp-equation nat-trans-assoc-comp-equation iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination functionExtensionality because_Cache sqequalRule dependent_functionElimination isect_memberEquality voidElimination voidEquality applyEquality setElimination rename natural_numberEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed productElimination independent_functionElimination

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))

Date html generated: 2020_05_20-AM-07_54_26
Last ObjectModification: 2017_07_28-AM-09_19_56

Theory : small!categories

Home Index