Nuprl Lemma : functor-ob_wf

[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (functor-ob(F) ∈ cat-ob(C) ⟶ cat-ob(D))


Proof




Definitions occuring in Statement :  functor-ob: functor-ob(F) cat-functor: Functor(C1;C2) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  pi1: fst(t) cat-functor: Functor(C1;C2) functor-ob: functor-ob(F) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-functor_wf
Rules used in proof :  because_Cache isect_memberEquality isectElimination 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,D:SmallCategory].  \mforall{}[F:Functor(C;D)].    (functor-ob(F)  \mmember{}  cat-ob(C)  {}\mrightarrow{}  cat-ob(D))



Date html generated: 2016_05_18-AM-11_52_17
Last ObjectModification: 2015_12_28-PM-02_23_56

Theory : small!categories


Home Index