Nuprl Lemma : functor-presheaf_wf

[C,D:SmallCategory].  ∀F:Functor(C;D). ∀P:Presheaf(D).  (functor-presheaf(F;P) ∈ Presheaf(C))


Proof




Definitions occuring in Statement :  functor-presheaf: functor-presheaf(F;P) presheaf: Presheaf(C) cat-functor: Functor(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T
Definitions unfolded in proof :  subtype_rel: A ⊆B functor-presheaf: functor-presheaf(F;P) presheaf: Presheaf(C) all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-functor_wf presheaf_wf op-functor_wf type-cat_wf small-category-subtype op-cat_wf functor-comp_wf
Rules used in proof :  isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality dependent_functionElimination lambdaEquality because_Cache sqequalRule hypothesis applyEquality hypothesisEquality isectElimination extract_by_obid instantiate thin sqequalHypSubstitution lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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



Date html generated: 2017_10_05-PM-03_34_10
Last ObjectModification: 2017_10_05-AM-11_37_40

Theory : small!categories


Home Index