Nuprl Lemma : cat-square-commutes-comp

[C:SmallCategory]. ∀[x1,x2,x3,y1,y2,y3:cat-ob(C)]. ∀[x1_y1:cat-arrow(C) x1 y1]. ∀[x2_y2:cat-arrow(C) x2 y2].
[x3_y3:cat-arrow(C) x3 y3]. ∀[y1_y2:cat-arrow(C) y1 y2]. ∀[y2_y3:cat-arrow(C) y2 y3]. ∀[x1_x2:cat-arrow(C) x1 x2].
[x2_x3:cat-arrow(C) x2 x3].
  (x1_y1 cat-comp(C) y1 y2 y3 y1_y2 y2_y3 cat-comp(C) x1 x2 x3 x1_x2 x2_x3 x3_y3) supposing 
     (x1_y1 y1_y2 x1_x2 x2_y2 and 
     x2_y2 y2_y3 x2_x3 x3_y3)


Definitions occuring in Statement :  cat-square-commutes: x_y1 y1_z x_y2 y2_z cat-comp: cat-comp(C) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uimplies: supposing a uall: [x:A]. B[x] apply: a
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a cat-square-commutes: x_y1 y1_z x_y2 y2_z squash: T prop: all: x:A. B[x] true: True subtype_rel: A ⊆B 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-square-commutes_wf cat-ob_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution applyEquality thin lambdaEquality imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality dependent_functionElimination because_Cache natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination axiomEquality isect_memberEquality

\mforall{}[C:SmallCategory].  \mforall{}[x1,x2,x3,y1,y2,y3:cat-ob(C)].  \mforall{}[x1$_{y1}$:cat-arrow(C)  x1  \000Cy1].  \mforall{}[x2$_{y2}$:cat-arrow(C) 
\mforall{}[x3$_{y3}$:cat-arrow(C)  x3  y3].  \mforall{}[y1$_{y2}$:cat-arrow(C)  y1\000C  y2].  \mforall{}[y2$_{y3}$:cat-arrow(C)  y2  y3].
\mforall{}[x1$_{x2}$:cat-arrow(C)  x1  x2].  \mforall{}[x2$_{x3}$:cat-arrow(C)  x2\000C  x3].
    (x1$_{y1}$  o  cat-comp(C)  y1  y2  y3  y1$_{y2}$  y2$_\mbackslash{}f\000Cf7by3}$  =  cat-comp(C)  x1  x2  x3  x1$_{x2}$  x2$_{x3}$  o\000C  x3$_{y3}$)  supposing 
          (x1$_{y1}$  o  y1$_{y2}$  =  x1$_{x2}$  \000Co  x2$_{y2}$  and 
          x2$_{y2}$  o  y2$_{y3}$  =  x2$_{x3}$  o\000C  x3$_{y3}$)

Date html generated: 2017_10_05-AM-00_49_00
Last ObjectModification: 2017_07_28-AM-09_20_05

Theory : small!categories

Home Index