### Nuprl Lemma : mk-presheaf_wf

`∀[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ Type]. ∀[morph:I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ S[I] ⟶ S[J]].`
`  (Presheaf(Set(I) =S[I];`
`            Morphism(I,J,f,rho) = morph[I;J;f;rho]) ∈ Presheaf(C)) supposing `
`     ((∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀rho:S[I].`
`         (morph[I;K;cat-comp(C) K J I g f;rho] = morph[J;K;g;morph[I;J;f;rho]] ∈ S[K])) and `
`     (∀I:cat-ob(C). ∀rho:S[I].  (morph[I;I;cat-id(C) I;rho] = rho ∈ S[I])))`

Proof

Definitions occuring in Statement :  mk-presheaf: mk-presheaf presheaf: `Presheaf(C)` cat-comp: `cat-comp(C)` cat-id: `cat-id(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2;s3;s4]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` uimplies: `b supposing a` all: `∀x:A. B[x]` top: `Top` type-cat: `TypeCat` so_apply: `x[s1;s2;s3;s4]` compose: `f o g` squash: `↓T` prop: `ℙ` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` mk-presheaf: mk-presheaf presheaf: `Presheaf(C)` so_lambda: `λ2x.t[x]` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]`
Lemmas referenced :  op-cat_wf small-category-subtype type-cat_wf subtype_rel-equal cat-ob_wf cat_ob_op_lemma op-cat-arrow cat_arrow_triple_lemma cat-arrow_wf op-cat-comp cat_comp_tuple_lemma equal_wf squash_wf true_wf iff_weakening_equal op-cat-id cat_id_tuple_lemma mk-functor_wf all_wf cat-comp_wf cat-id_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality hypothesis sqequalRule functionExtensionality because_Cache independent_isectElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaEquality lambdaFormation imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination isect_memberFormation axiomEquality functionEquality cumulativity

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[S:cat-ob(C)  {}\mrightarrow{}  Type].  \mforall{}[morph:I:cat-ob(C)
{}\mrightarrow{}  J:cat-ob(C)
{}\mrightarrow{}  f:(cat-arrow(C)  J  I)
{}\mrightarrow{}  S[I]
{}\mrightarrow{}  S[J]].
(Presheaf(Set(I)  =S[I];
Morphism(I,J,f,rho)  =  morph[I;J;f;rho])  \mmember{}  Presheaf(C))  supposing
((\mforall{}I,J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}rho:S[I].
(morph[I;K;cat-comp(C)  K  J  I  g  f;rho]  =  morph[J;K;g;morph[I;J;f;rho]]))  and
(\mforall{}I:cat-ob(C).  \mforall{}rho:S[I].    (morph[I;I;cat-id(C)  I;rho]  =  rho)))

Date html generated: 2020_05_20-AM-07_52_56
Last ObjectModification: 2017_10_03-PM-01_57_52

Theory : small!categories

Home Index