### Nuprl Lemma : equal-presheaves

`∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].`
`  F = G ∈ Presheaf(C) `
`  supposing (∀x:cat-ob(op-cat(C)). ((F x) = (G x) ∈ cat-ob(TypeCat)))`
`  ∧ (∀x,y:cat-ob(op-cat(C)). ∀f:cat-arrow(op-cat(C)) x y.  ((F x y f) = (G x y f) ∈ (cat-arrow(TypeCat) (F x) (F y))))`

Proof

Definitions occuring in Statement :  presheaf: `Presheaf(C)` type-cat: `TypeCat` op-cat: `op-cat(C)` functor-arrow: `arrow(F)` functor-ob: `ob(F)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` presheaf: `Presheaf(C)` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` squash: `↓T` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  equal-functors op-cat_wf type-cat_wf all_wf cat-ob_wf equal_wf functor-ob_wf small-category-subtype cat-arrow_wf functor-arrow_wf subtype_rel-equal squash_wf true_wf iff_weakening_equal presheaf_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin instantiate extract_by_obid isectElimination hypothesisEquality applyEquality because_Cache hypothesis sqequalRule independent_isectElimination productEquality lambdaEquality cumulativity universeEquality imageElimination equalityTransitivity equalitySymmetry dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_functionElimination isect_memberEquality axiomEquality

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F,G:Presheaf(C)].
F  =  G
supposing  (\mforall{}x:cat-ob(op-cat(C)).  ((F  x)  =  (G  x)))
\mwedge{}  (\mforall{}x,y:cat-ob(op-cat(C)).  \mforall{}f:cat-arrow(op-cat(C))  x  y.    ((F  x  y  f)  =  (G  x  y  f)))

Date html generated: 2020_05_20-AM-07_53_29
Last ObjectModification: 2017_10_03-PM-02_24_56

Theory : small!categories

Home Index