Nuprl Lemma : trans-comp-assoc

C1,C2:SmallCategory. ∀x,y,z,w:Functor(C1;C2). ∀f:nat-trans(C1;C2;x;y). ∀g:nat-trans(C1;C2;y;z).
h:nat-trans(C1;C2;z;w).
  (f h ∈ nat-trans(C1;C2;x;w))


Proof




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

Latex:
\mforall{}C1,C2:SmallCategory.  \mforall{}x,y,z,w:Functor(C1;C2).  \mforall{}f:nat-trans(C1;C2;x;y).  \mforall{}g:nat-trans(C1;C2;y;z).
\mforall{}h:nat-trans(C1;C2;z;w).
    (f  o  g  o  h  =  f  o  g  o  h)



Date html generated: 2017_10_05-AM-00_46_17
Last ObjectModification: 2017_07_28-AM-09_19_22

Theory : small!categories


Home Index