### Nuprl Lemma : presheaf-subset-and

`∀[C:SmallCategory]. ∀[F:presheaf{j:l}(C)]. ∀[P,Q:I:cat-ob(C) ⟶ (F I) ⟶ ℙ].`
`  ext-equal-presheaves(C;F|I,rho.P[I;rho]|I,rho.Q[I;rho];F|I,rho.P[I;rho] ∧ Q[I;rho]) `
`  supposing stable-element-predicate(C;F;I,rho.P[I;rho]) ∧ stable-element-predicate(C;F;I,rho.Q[I;rho])`

Proof

Definitions occuring in Statement :  presheaf-subset: `F|I,rho.P[I; rho]` stable-element-predicate: `stable-element-predicate(C;F;I,rho.P[I; rho])` ext-equal-presheaves: `ext-equal-presheaves(C;F;G)` presheaf: `Presheaf(C)` functor-ob: `ob(F)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` ext-equal-presheaves: `ext-equal-presheaves(C;F;G)` all: `∀x:A. B[x]` presheaf-subset: `F|I,rho.P[I; rho]` mk-presheaf: mk-presheaf so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` ext-eq: `A ≡ B` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` so_apply: `x[s1;s2]` presheaf: `Presheaf(C)` cat-ob: `cat-ob(C)` pi1: `fst(t)` type-cat: `TypeCat` guard: `{T}` stable-element-predicate: `stable-element-predicate(C;F;I,rho.P[I; rho])` implies: `P `` Q`
Lemmas referenced :  small-category_wf ob_mk_functor_lemma arrow_mk_functor_lemma cat-arrow_wf stable-element-predicate_wf small-category-cumulativity-2 presheaf-cumulativity1 functor-ob_wf op-cat_wf type-cat_wf subtype_rel-equal cat-ob_wf cat_ob_op_lemma subtype_rel_self cat_ob_pair_lemma functor-arrow_wf op-cat-arrow presheaf_wf1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt universeIsType cut introduction extract_by_obid hypothesis sqequalHypSubstitution productElimination thin independent_pairFormation lambdaFormation_alt sqequalRule dependent_functionElimination Error :memTop,  because_Cache applyEquality isectElimination hypothesisEquality independent_pairEquality lambdaEquality_alt axiomEquality functionIsTypeImplies inhabitedIsType productIsType instantiate cumulativity independent_isectElimination universeEquality isect_memberEquality_alt isectIsTypeImplies functionIsType setElimination rename dependent_set_memberEquality_alt setIsType functionExtensionality setEquality independent_functionElimination

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F:presheaf\{j:l\}(C)].  \mforall{}[P,Q:I:cat-ob(C)  {}\mrightarrow{}  (F  I)  {}\mrightarrow{}  \mBbbP{}].
ext-equal-presheaves(C;F|I,rho.P[I;rho]|I,rho.Q[I;rho];F|I,rho.P[I;rho]  \mwedge{}  Q[I;rho])
supposing  stable-element-predicate(C;F;I,rho.P[I;rho])
\mwedge{}  stable-element-predicate(C;F;I,rho.Q[I;rho])

Date html generated: 2020_05_20-AM-07_57_39
Last ObjectModification: 2020_04_02-AM-09_48_25

Theory : small!categories

Home Index