### Nuprl Lemma : respects-equality-quotient1

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

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

Date html generated: 2019_06_20-PM-00_32_26
Last ObjectModification: 2018_12_13-PM-04_09_24

Theory : quot_1

Home Index