### Nuprl Lemma : respects-equality-quotient

`∀[X,T:Type]. ∀[E1:X ⟶ X ⟶ ℙ]. ∀[E2:T ⟶ T ⟶ ℙ].`
`  (respects-equality(x,y:X//E1[x;y];x,y:T//E2[x;y])) supposing `
`     ((∀x,y:X.  (E1[x;y] `` (x ∈ T) `` ((y ∈ T) ∧ E2[x;y]))) and `
`     respects-equality(X;T) and `
`     EquivRel(X;x,y.E1[x;y]) and `
`     EquivRel(T;x,y.E2[x;y]))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` uimplies: `b supposing a` respects-equality: `respects-equality(S;T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` sq_stable: `SqStable(P)` implies: `P `` Q` respects-equality: `respects-equality(S;T)` all: `∀x:A. B[x]` squash: `↓T` subtype_rel: `A ⊆r B` prop: `ℙ` and: `P ∧ Q` quotient: `x,y:A//B[x; y]` cand: `A c∧ B`
Lemmas referenced :  sq_stable__respects-equality quotient_wf istype-base subtype_rel_self respects-equality_wf equiv_rel_wf istype-universe quotient-member-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  applyEquality because_Cache independent_isectElimination hypothesis independent_functionElimination Error :lambdaFormation_alt,  Error :equalityIstype,  Error :universeIsType,  sqequalBase equalitySymmetry imageMemberEquality baseClosed imageElimination Error :functionIsType,  instantiate dependent_functionElimination Error :productIsType,  universeEquality Error :inhabitedIsType,  pertypeElimination promote_hyp productElimination equalityTransitivity

Latex:
\mforall{}[X,T:Type].  \mforall{}[E1:X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(respects-equality(x,y:X//E1[x;y];x,y:T//E2[x;y]))  supposing
((\mforall{}x,y:X.    (E1[x;y]  {}\mRightarrow{}  (x  \mmember{}  T)  {}\mRightarrow{}  ((y  \mmember{}  T)  \mwedge{}  E2[x;y])))  and
respects-equality(X;T)  and
EquivRel(X;x,y.E1[x;y])  and
EquivRel(T;x,y.E2[x;y]))

Date html generated: 2019_06_20-PM-00_32_24
Last ObjectModification: 2018_11_29-PM-07_01_37

Theory : quot_1

Home Index