Nuprl Lemma : full-faithful-functor_wf

[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (ff-functor(C;D;F) ∈ ℙ)


Proof




Definitions occuring in Statement :  full-faithful-functor: ff-functor(C;D;F) cat-functor: Functor(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  so_apply: x[s] so_lambda: λ2x.t[x] full-faithful-functor: ff-functor(C;D;F) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-functor_wf functor-arrow_wf functor-ob_wf cat-arrow_wf biject_wf cat-ob_wf all_wf
Rules used in proof :  because_Cache isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality applyEquality lambdaEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution lemma_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].    (ff-functor(C;D;F)  \mmember{}  \mBbbP{})



Date html generated: 2016_05_18-AM-11_52_27
Last ObjectModification: 2015_12_28-PM-02_23_53

Theory : small!categories


Home Index