Nuprl Lemma : trans-horizontal-comp_wf

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

Latex:
\mforall{}[C,D,E:SmallCategory].  \mforall{}[F,G:Functor(C;D)].  \mforall{}[J,K:Functor(D;E)].  \mforall{}[tFG:nat-trans(C;D;F;G)].
\mforall{}[tJK:nat-trans(D;E;J;K)].
(trans-horizontal-comp(E;F;G;J;K;tFG;tJK)  \mmember{}  nat-trans(C;E;functor-comp(F;J);functor-comp(G;K)))

Date html generated: 2020_05_20-AM-07_54_23
Last ObjectModification: 2017_07_28-AM-09_19_54

Theory : small!categories

Home Index