### Nuprl Lemma : cat_comp_assoc

[C:SmallCategory]
∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) y. ∀g:cat-arrow(C) z. ∀h:cat-arrow(C) w.
(h f ∈ (cat-arrow(C) w))

Proof

Definitions occuring in Statement :  cat_comp: f cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] all: x:A. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  cat_comp: f uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  equal_wf squash_wf true_wf cat-arrow_wf cat-comp-assoc cat-comp_wf iff_weakening_equal cat-ob_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaFormation applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality dependent_functionElimination because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination axiomEquality

Latex:
\mforall{}[C:SmallCategory]
\mforall{}x,y,z,w:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.  \mforall{}g:cat-arrow(C)  y  z.  \mforall{}h:cat-arrow(C)  z  w.
(h  o  g  o  f  =  h  o  g  o  f)

Date html generated: 2017_10_05-AM-00_45_39
Last ObjectModification: 2017_07_28-AM-09_19_01

Theory : small!categories

Home Index