### Nuprl Lemma : cat-comp-ident

`∀[C:SmallCategory]`
`  ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.`
`    (((cat-comp(C) x x y (cat-id(C) x) f) = f ∈ (cat-arrow(C) x y))`
`    ∧ ((cat-comp(C) x y y f (cat-id(C) y)) = f ∈ (cat-arrow(C) x y)))`

Proof

Definitions occuring in Statement :  cat-comp: `cat-comp(C)` cat-id: `cat-id(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` 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}` cand: `A c∧ B` and: `P ∧ Q` spreadn: spread4 cat-comp: `cat-comp(C)` cat-id: `cat-id(C)` cat-ob: `cat-ob(C)` pi1: `fst(t)` pi2: `snd(t)` cat-arrow: `cat-arrow(C)` small-category: `SmallCategory` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  small-category_wf cat-ob_wf cat-arrow_wf
Rules used in proof :  because_Cache axiomEquality independent_pairEquality dependent_functionElimination lambdaEquality hypothesisEquality isectElimination lemma_by_obid applyEquality hypothesis independent_pairFormation sqequalRule productElimination rename thin setElimination sqequalHypSubstitution lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C:SmallCategory]
\mforall{}x,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.
(((cat-comp(C)  x  x  y  (cat-id(C)  x)  f)  =  f)  \mwedge{}  ((cat-comp(C)  x  y  y  f  (cat-id(C)  y))  =  f))

Date html generated: 2016_05_18-AM-11_52_12
Last ObjectModification: 2015_12_28-PM-02_23_55

Theory : small!categories

Home Index