### Nuprl Lemma : groupoid_inv

`∀[G:Groupoid]`
`  ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) x y.`
`    (((cat-comp(cat(G)) x y x f groupoid-inv(G;x;y;f)) = (cat-id(cat(G)) x) ∈ (cat-arrow(cat(G)) x x))`
`    ∧ ((cat-comp(cat(G)) y x y groupoid-inv(G;x;y;f) f) = (cat-id(cat(G)) y) ∈ (cat-arrow(cat(G)) y y)))`

Proof

Definitions occuring in Statement :  groupoid-inv: `groupoid-inv(G;x;y;x_y)` groupoid-cat: `cat(G)` groupoid: `Groupoid` cat-comp: `cat-comp(C)` cat-id: `cat-id(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  guard: `{T}` pi2: `snd(t)` groupoid-inv: `groupoid-inv(G;x;y;x_y)` pi1: `fst(t)` groupoid-cat: `cat(G)` groupoid: `Groupoid` cand: `A c∧ B` and: `P ∧ Q` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  groupoid_wf cat-ob_wf groupoid-cat_wf cat-arrow_wf
Rules used in proof :  because_Cache axiomEquality independent_pairEquality dependent_functionElimination lambdaEquality hypothesisEquality isectElimination lemma_by_obid applyEquality independent_pairFormation hypothesis sqequalRule rename setElimination thin productElimination sqequalHypSubstitution lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[G:Groupoid]
\mforall{}x,y:cat-ob(cat(G)).  \mforall{}f:cat-arrow(cat(G))  x  y.
(((cat-comp(cat(G))  x  y  x  f  groupoid-inv(G;x;y;f))  =  (cat-id(cat(G))  x))
\mwedge{}  ((cat-comp(cat(G))  y  x  y  groupoid-inv(G;x;y;f)  f)  =  (cat-id(cat(G))  y)))

Date html generated: 2016_05_18-AM-11_54_28
Last ObjectModification: 2015_12_28-PM-02_23_11

Theory : small!categories

Home Index