### Nuprl Lemma : mk-presheaf_wf1

`∀[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ 𝕌{j}]. ∀[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{j:l}(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]` cat-ob: `cat-ob(C)` pi1: `fst(t)` type-cat: `TypeCat` so_apply: `x[s1;s2;s3;s4]` compose: `f o g` guard: `{T}` 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-cumulativity-2 type-cat_wf subtype_rel-equal cat-ob_wf cat_ob_op_lemma subtype_rel_self op-cat-arrow cat_arrow_triple_lemma cat-arrow_wf op-cat-comp cat_comp_tuple_lemma op-cat-id cat_id_tuple_lemma mk-functor_wf cat-comp_wf cat-id_wf istype-universe small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality hypothesis sqequalRule because_Cache independent_isectElimination dependent_functionElimination universeIsType Error :memTop,  lambdaEquality_alt lambdaFormation_alt functionExtensionality_alt isect_memberFormation_alt axiomEquality equalityTransitivity equalitySymmetry functionIsType equalityIstype isect_memberEquality_alt isectIsTypeImplies inhabitedIsType universeEquality

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[S:cat-ob(C)  {}\mrightarrow{}  \mBbbU{}\{j\}].  \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\{j:l\}(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_54
Last ObjectModification: 2020_04_03-AM-11_26_55

Theory : small!categories

Home Index