### Nuprl Lemma : cat-comp-assoc

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

Proof

Definitions occuring in Statement :  cat-comp: `cat-comp(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` small-category: `SmallCategory` cat-arrow: `cat-arrow(C)` pi2: `snd(t)` pi1: `fst(t)` cat-ob: `cat-ob(C)` cat-comp: `cat-comp(C)` spreadn: spread4 and: `P ∧ Q` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  equal_wf squash_wf true_wf iff_weakening_equal cat-arrow_wf cat-ob_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution setElimination thin rename productElimination sqequalRule applyEquality lambdaEquality imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality functionExtensionality cumulativity dependent_functionElimination because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination 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.
((cat-comp(C)  x  z  w  (cat-comp(C)  x  y  z  f  g)  h)  =  (cat-comp(C)  x  y  w  f  (cat-comp(C)  y  z  w  g  h)))

Date html generated: 2020_05_20-AM-07_49_57
Last ObjectModification: 2017_07_28-AM-09_18_59

Theory : small!categories

Home Index