### Nuprl Lemma : trans-id-property

`∀C1,C2:SmallCategory. ∀x,y:Functor(C1;C2). ∀f:nat-trans(C1;C2;x;y).`
`  ((identity-trans(C1;C2;x) o f = f ∈ nat-trans(C1;C2;x;y)) ∧ (f o identity-trans(C1;C2;y) = f ∈ nat-trans(C1;C2;x;y)))`

Proof

Definitions occuring in Statement :  trans-comp: `t1 o t2` identity-trans: `identity-trans(C;D;F)` nat-trans: `nat-trans(C;D;F;G)` cat-functor: `Functor(C1;C2)` small-category: `SmallCategory` all: `∀x:A. B[x]` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` nat-trans: `nat-trans(C;D;F;G)` identity-trans: `identity-trans(C;D;F)` trans-comp: `t1 o t2` member: `t ∈ T` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uall: `∀[x:A]. B[x]` prop: `ℙ`
Lemmas referenced :  ap_mk_nat_trans_lemma cat-comp-ident functor-ob_wf cat-ob_wf all_wf cat-arrow_wf equal_wf cat-comp_wf functor-arrow_wf nat-trans_wf cat-functor_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution setElimination thin rename equalitySymmetry dependent_set_memberEquality functionExtensionality sqequalRule introduction extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality hypothesis isectElimination hypothesisEquality applyEquality productElimination lambdaEquality because_Cache independent_pairFormation

Latex:
\mforall{}C1,C2:SmallCategory.  \mforall{}x,y:Functor(C1;C2).  \mforall{}f:nat-trans(C1;C2;x;y).
((identity-trans(C1;C2;x)  o  f  =  f)  \mwedge{}  (f  o  identity-trans(C1;C2;y)  =  f))

Date html generated: 2020_05_20-AM-07_51_44
Last ObjectModification: 2017_01_10-PM-04_46_00

Theory : small!categories

Home Index