Nuprl Lemma : id_functor_wf

[A:SmallCategory]. (1 ∈ Functor(A;A))


Proof




Definitions occuring in Statement :  id_functor: 1 cat-functor: Functor(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a id_functor: 1 member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-id_wf cat-comp_wf cat-arrow_wf cat-ob_wf
Rules used in proof :  equalitySymmetry equalityTransitivity axiomEquality lambdaFormation independent_isectElimination applyEquality hypothesis lambdaEquality because_Cache hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[A:SmallCategory].  (1  \mmember{}  Functor(A;A))



Date html generated: 2020_05_20-AM-07_53_35
Last ObjectModification: 2018_05_18-PM-04_41_59

Theory : small!categories


Home Index