### 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: 2020_05_20-AM-07_51_12
Last ObjectModification: 2015_12_28-PM-02_23_53

Theory : small!categories

Home Index