### Nuprl Lemma : trans-id-property

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

Proof

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

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

Date html generated: 2017_01_11-AM-09_18_21
Last ObjectModification: 2017_01_10-PM-04_46_00

Theory : small!categories

Home Index