### Nuprl Lemma : ext-equal-presheaves-equiv-rel

`∀[C:SmallCategory]. EquivRel(Presheaf(C);F,G.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` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` ext-equal-presheaves: `ext-equal-presheaves(C;F;G)` ext-eq: `A ≡ B` subtype_rel: `A ⊆r B` presheaf: `Presheaf(C)` uimplies: `b supposing a` top: `Top` cat-arrow: `cat-arrow(C)` pi1: `fst(t)` pi2: `snd(t)` type-cat: `TypeCat` cat-ob: `cat-ob(C)` guard: `{T}`
Lemmas referenced :  presheaf_wf ext-equal-presheaves_wf cat-ob_wf cat-arrow_wf small-category_wf ext-eq_weakening functor-ob_wf op-cat_wf small-category-subtype type-cat_wf subtype_rel-equal cat_ob_op_lemma functor-arrow_wf op-cat-arrow subtype_rel_self subtype_rel_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache sqequalRule productElimination independent_pairEquality lambdaEquality dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry applyEquality instantiate independent_isectElimination isect_memberEquality voidElimination voidEquality functionEquality functionExtensionality applyLambdaEquality universeEquality

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

Date html generated: 2017_10_05-AM-00_47_00
Last ObjectModification: 2017_10_03-PM-02_53_58

Theory : small!categories

Home Index