Nuprl Lemma : yoneda-lemma

C:SmallCategory. ff-functor(C;FUN(op-cat(C);TypeCat);yoneda-embedding(C))


Proof




Definitions occuring in Statement :  yoneda-embedding: yoneda-embedding(C) type-cat: TypeCat op-cat: op-cat(C) functor-cat: FUN(C1;C2) full-faithful-functor: ff-functor(C;D;F) small-category: SmallCategory all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] full-faithful-functor: ff-functor(C;D;F) biject: Bij(A;B;f) and: P ∧ Q inject: Inj(A;B;f) implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] subtype_rel: A ⊆B surject: Surj(A;B;f) yoneda-embedding: yoneda-embedding(C) top: Top so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] so_lambda: λ2x.t[x] so_apply: x[s] nat-trans: nat-trans(C;D;F;G) squash: T uimplies: supposing a cat-arrow: cat-arrow(C) pi1: fst(t) pi2: snd(t) type-cat: TypeCat functor-ob: ob(F) rep-pre-sheaf: rep-pre-sheaf(C;X) true: True guard: {T} iff: ⇐⇒ Q exists: x:A. B[x] mk-functor: mk-functor functor-cat: FUN(C1;C2) functor-arrow: arrow(F) compose: g
Lemmas referenced :  equal_wf cat-arrow_wf functor-cat_wf op-cat_wf small-category-subtype type-cat_wf functor-ob_wf yoneda-embedding_wf functor-arrow_wf cat-ob_wf small-category_wf functor_cat_arrow_lemma ob_mk_functor_lemma arrow_mk_functor_lemma subtype_rel-equal cat_ob_op_lemma subtype_rel_self rep-pre-sheaf_wf cat-id_wf ap_mk_nat_trans_lemma squash_wf true_wf cat-comp-ident1 iff_weakening_equal functor_cat_ob_lemma cat_arrow_triple_lemma nat-trans-equal op-cat-arrow cat_comp_tuple_lemma cat-comp_wf cat-comp-ident2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut hypothesis thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination applyEquality hypothesisEquality sqequalRule because_Cache dependent_functionElimination isect_memberEquality voidElimination voidEquality applyLambdaEquality setElimination rename imageMemberEquality baseClosed imageElimination functionExtensionality independent_isectElimination functionEquality natural_numberEquality lambdaEquality equalityTransitivity equalitySymmetry universeEquality productElimination independent_functionElimination dependent_pairFormation

Latex:
\mforall{}C:SmallCategory.  ff-functor(C;FUN(op-cat(C);TypeCat);yoneda-embedding(C))



Date html generated: 2017_10_05-AM-00_47_20
Last ObjectModification: 2017_07_28-AM-09_19_38

Theory : small!categories


Home Index