Nuprl Lemma : left-right-inverse-unique
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g2:cat-arrow(C) y x].
∀[g1:cat-arrow(C) y x]. g1 = g2 ∈ (cat-arrow(C) y x) supposing fg1=1 supposing g2f=1
Proof
Definitions occuring in Statement :
cat-inverse: fg=1,
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,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
prop: ℙ,
cat-inverse: fg=1,
true: True,
squash: ↓T,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
cat-inverse_wf,
cat-arrow_wf,
cat-ob_wf,
small-category_wf,
cat-comp_wf,
equal_wf,
squash_wf,
true_wf,
iff_weakening_equal,
cat-comp-ident,
cat-comp-assoc
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
hypothesis,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
isect_memberEquality,
axiomEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
applyEquality,
natural_numberEquality,
lambdaEquality,
imageElimination,
universeEquality,
imageMemberEquality,
baseClosed,
independent_isectElimination,
productElimination,
independent_functionElimination,
dependent_functionElimination
Latex:
\mforall{}[C:SmallCategory]. \mforall{}[x,y:cat-ob(C)]. \mforall{}[f:cat-arrow(C) x y]. \mforall{}[g2:cat-arrow(C) y x].
\mforall{}[g1:cat-arrow(C) y x]. g1 = g2 supposing fg1=1 supposing g2f=1
Date html generated:
2020_05_20-AM-07_50_04
Last ObjectModification:
2017_07_28-AM-09_19_02
Theory : small!categories
Home
Index