Nuprl Lemma : cat-id_wf

[C:SmallCategory]. (cat-id(C) ∈ x:cat-ob(C) ⟶ (cat-arrow(C) x))


Proof




Definitions occuring in Statement :  cat-id: cat-id(C) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) spreadn: spread4 pi2: snd(t) pi1: fst(t) small-category: SmallCategory cat-id: cat-id(C) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf
Rules used in proof :  lemma_by_obid equalitySymmetry equalityTransitivity axiomEquality hypothesis hypothesisEquality productElimination rename thin setElimination sqequalHypSubstitution sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C:SmallCategory].  (cat-id(C)  \mmember{}  x:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  x  x))



Date html generated: 2016_05_18-AM-11_52_03
Last ObjectModification: 2015_12_28-PM-02_24_05

Theory : small!categories


Home Index