Nuprl Lemma : ext-equal-presheaves_wf

[C:SmallCategory]. ∀[F,G:Presheaf(C)].  (ext-equal-presheaves(C;F;G) ∈ ℙ')


Proof




Definitions occuring in Statement :  ext-equal-presheaves: ext-equal-presheaves(C;F;G) presheaf: Presheaf(C) small-category: SmallCategory uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ext-equal-presheaves: ext-equal-presheaves(C;F;G) prop: and: P ∧ Q so_lambda: λ2x.t[x] subtype_rel: A ⊆B presheaf: Presheaf(C) uimplies: supposing a all: x:A. B[x] so_apply: x[s] top: Top cat-arrow: cat-arrow(C) pi1: fst(t) pi2: snd(t) type-cat: TypeCat ext-eq: A ≡ B
Lemmas referenced :  all_wf cat-ob_wf ext-eq_wf functor-ob_wf op-cat_wf small-category-subtype type-cat_wf subtype_rel-equal cat_ob_op_lemma cat-arrow_wf equal_wf functor-arrow_wf op-cat-arrow subtype_rel_self presheaf_wf small-category_wf cat_arrow_triple_lemma subtype_rel_dep_function
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality applyEquality instantiate because_Cache independent_isectElimination dependent_functionElimination cumulativity universeEquality functionEquality isect_memberEquality voidElimination voidEquality axiomEquality equalityTransitivity equalitySymmetry productElimination lambdaFormation

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F,G:Presheaf(C)].    (ext-equal-presheaves(C;F;G)  \mmember{}  \mBbbP{}')



Date html generated: 2017_10_05-AM-00_46_54
Last ObjectModification: 2017_10_03-PM-02_38_54

Theory : small!categories


Home Index