Nuprl Lemma : extend-type-property

[T:Type]. ((T ⊆(T)+) ∧ respects-equality((T)+;T) ∧ (∀X:Type. (respects-equality(X;T)  (X ⊆(T)+))))


Proof




Definitions occuring in Statement :  extend-type: (T)+ subtype_rel: A ⊆B respects-equality: respects-equality(S;T) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] and: P ∧ Q member: t ∈ T subtype_rel: A ⊆B extend-type: (T)+ so_lambda: λ2y.t[x; y] prop: iff: ⇐⇒ Q rev_implies:  Q implies:  Q so_apply: x[s1;s2] uimplies: supposing a all: x:A. B[x] cand: c∧ B respects-equality: respects-equality(S;T) quotient: x,y:A//B[x; y]
Lemmas referenced :  istype-universe extend-type_wf quotient-member-eq base_wf iff_wf equal-wf-base equal-wf-T-base extend-type-equiv istype-base respects-equality_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  independent_pairFormation cut instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination thin universeEquality hypothesis Error :lambdaEquality_alt,  Error :universeIsType,  hypothesisEquality pointwiseFunctionalityForEquality sqequalRule productEquality because_Cache functionEquality Error :inhabitedIsType,  independent_isectElimination dependent_functionElimination independent_functionElimination Error :lambdaFormation_alt,  equalityTransitivity equalitySymmetry Error :equalityIstype,  sqequalBase productElimination pertypeElimination promote_hyp Error :productIsType,  Error :functionIsType,  axiomEquality

Latex:
\mforall{}[T:Type]
    ((T  \msubseteq{}r  (T)+)  \mwedge{}  respects-equality((T)+;T)  \mwedge{}  (\mforall{}X:Type.  (respects-equality(X;T)  {}\mRightarrow{}  (X  \msubseteq{}r  (T)+))))



Date html generated: 2019_06_20-PM-00_33_29
Last ObjectModification: 2018_11_25-PM-06_55_25

Theory : quot_1


Home Index