Nuprl Lemma : yoneda-embedding_wf

[C:SmallCategory]. (yoneda-embedding(C) ∈ Functor(C;FUN(op-cat(C);TypeCat)))


Proof




Definitions occuring in Statement :  yoneda-embedding: yoneda-embedding(C) type-cat: TypeCat op-cat: op-cat(C) functor-cat: FUN(C1;C2) cat-functor: Functor(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] yoneda-embedding: yoneda-embedding(C) member: t ∈ T subtype_rel: A ⊆B all: x:A. B[x] top: Top so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a so_lambda: so_lambda3 so_apply: x[s1;s2;s3] rep-pre-sheaf: rep-pre-sheaf(C;X) functor-ob: ob(F) type-cat: TypeCat pi1: fst(t) functor-arrow: arrow(F) pi2: snd(t) compose: g true: True squash: T prop: guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q trans-comp: t1 t2 identity-trans: identity-trans(C;D;F)
Lemmas referenced :  small-category_wf small-category-subtype functor-cat_wf op-cat_wf type-cat_wf functor_cat_ob_lemma rep-pre-sheaf_wf cat-ob_wf functor_cat_arrow_lemma mk-nat-trans_wf cat-arrow_wf functor_cat_comp_lemma functor_cat_id_lemma mk-functor_wf cat_arrow_triple_lemma cat-comp_wf subtype_rel-equal cat_ob_op_lemma cat_comp_tuple_lemma op-cat-arrow equal_wf squash_wf true_wf cat-comp-assoc iff_weakening_equal ap_mk_nat_trans_lemma all_wf functor-ob_wf functor-arrow_wf cat-functor_wf cat_id_tuple_lemma cat-comp-ident
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid hypothesis hypothesisEquality applyEquality sqequalHypSubstitution sqequalRule thin instantiate isectElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality because_Cache lambdaEquality independent_isectElimination lambdaFormation functionExtensionality natural_numberEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed productElimination independent_functionElimination functionEquality

Latex:
\mforall{}[C:SmallCategory].  (yoneda-embedding(C)  \mmember{}  Functor(C;FUN(op-cat(C);TypeCat)))



Date html generated: 2020_05_20-AM-07_53_12
Last ObjectModification: 2017_07_28-AM-09_19_36

Theory : small!categories


Home Index