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 


Definitions occuring in Statement :  equiv_rel: EquivRel(T;x,y.E[x; y]) quotient: x,y:A//B[x; y] uimplies: 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:  Q and: P ∧ Q member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] sq_stable: SqStable(P) implies:  Q respects-equality: respects-equality(S;T) all: x:A. B[x] squash: T subtype_rel: A ⊆B prop: and: P ∧ Q quotient: x,y:A//B[x; y] cand: 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

\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 

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

Theory : quot_1

Home Index