Nuprl Lemma : groupoid-square-commutes-iff
∀[G:Groupoid]. ∀[x,y1,y2,z:cat-ob(cat(G))]. ∀[x_y1:cat-arrow(cat(G)) x y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
∀[x_y2:cat-arrow(cat(G)) x y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
uiff(x_y1 o y1_z = x_y2 o y2_z;y2_z
= (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y1 z x_y1 y1_z))
∈ (cat-arrow(cat(G)) y2 z))
Proof
Definitions occuring in Statement :
groupoid-inv: groupoid-inv(G;x;y;x_y),
groupoid-cat: cat(G),
groupoid: Groupoid,
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),
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
apply: f a,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
cat-square-commutes: x_y1 o y1_z = x_y2 o y2_z,
prop: ℙ,
true: True,
squash: ↓T,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q
Lemmas referenced :
equal_wf,
cat-arrow_wf,
groupoid-cat_wf,
cat-comp_wf,
groupoid-inv_wf,
cat-square-commutes_wf,
cat-ob_wf,
groupoid_wf,
cat-comp-ident1,
iff_weakening_equal,
squash_wf,
true_wf,
cat-comp-assoc,
groupoid_inv
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
independent_pairFormation,
sqequalHypSubstitution,
hypothesis,
thin,
hyp_replacement,
equalitySymmetry,
applyLambdaEquality,
extract_by_obid,
isectElimination,
applyEquality,
hypothesisEquality,
because_Cache,
sqequalRule,
axiomEquality,
productElimination,
independent_pairEquality,
isect_memberEquality,
equalityTransitivity,
natural_numberEquality,
lambdaEquality,
imageElimination,
dependent_functionElimination,
imageMemberEquality,
baseClosed,
independent_isectElimination,
independent_functionElimination,
universeEquality
Latex:
\mforall{}[G:Groupoid]. \mforall{}[x,y1,y2,z:cat-ob(cat(G))]. \mforall{}[x$_{y1}$:cat-arrow(cat(G)) x y1]. \000C\mforall{}[y1$_{z}$:cat-arrow(cat(G))
y1
z].
\mforall{}[x$_{y2}$:cat-arrow(cat(G)) x y2]. \mforall{}[y2$_{z}$:cat-arrow(cat\000C(G)) y2 z].
uiff(x$_{y1}$ o y1$_{z}$ = x$_{y2}$ o \000Cy2$_{z}$;y2$_{z}$
= (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x$_{y2}$) (cat-comp(cat(G)) x y\000C1 z x$_{y1}$ y1$_{z}$)))
Date html generated:
2017_10_05-AM-00_49_20
Last ObjectModification:
2017_07_28-AM-09_20_16
Theory : small!categories
Home
Index