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 o cat-comp(C) y1 y2 y3 y1_y2 y2_y3 = cat-comp(C) x1 x2 x3 x1_x2 x2_x3 o x3_y3) supposing
(x1_y1 o y1_y2 = x1_x2 o x2_y2 and
x2_y2 o y2_y3 = x2_x3 o x3_y3)
Proof
Definitions occuring in Statement :
cat-square-commutes: x_y1 o y1_z = x_y2 o y2_z,
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
small-category: SmallCategory,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
cat-square-commutes: x_y1 o y1_z = x_y2 o y2_z,
squash: ↓T,
prop: ℙ,
all: ∀x:A. B[x],
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ 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
Latex:
\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)
x2
y2].
\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