Nuprl Lemma : strong-subtype-iff-respects-equality
∀[A,B:Type]. uiff(strong-subtype(A;B);(A ⊆r B) ∧ respects-equality(B;A))
Proof
Definitions occuring in Statement :
strong-subtype: strong-subtype(A;B)
,
uiff: uiff(P;Q)
,
subtype_rel: A ⊆r B
,
respects-equality: respects-equality(S;T)
,
uall: ∀[x:A]. B[x]
,
and: P ∧ Q
,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x]
,
uiff: uiff(P;Q)
,
and: P ∧ Q
,
uimplies: b supposing a
,
member: t ∈ T
,
strong-subtype: strong-subtype(A;B)
,
cand: A c∧ B
,
subtype_rel: A ⊆r B
,
respects-equality: respects-equality(S;T)
,
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
prop: ℙ
,
exists: ∃x:A. B[x]
Lemmas referenced :
strong-subtype_wf,
subtype_rel_wf,
respects-equality_wf,
istype-universe,
istype-base,
subtype-respects-equality
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
independent_pairFormation,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
independent_pairEquality,
axiomEquality,
hypothesis,
Error :lambdaEquality_alt,
dependent_functionElimination,
hypothesisEquality,
Error :functionIsTypeImplies,
Error :inhabitedIsType,
Error :universeIsType,
extract_by_obid,
isectElimination,
Error :productIsType,
instantiate,
universeEquality,
Error :lambdaFormation_alt,
Error :equalityIstype,
sqequalBase,
equalitySymmetry,
because_Cache,
applyEquality,
Error :dependent_set_memberEquality_alt,
equalityTransitivity,
independent_isectElimination,
independent_functionElimination,
Error :dependent_pairFormation_alt,
setElimination,
rename,
Error :setIsType,
pointwiseFunctionalityForEquality
Latex:
\mforall{}[A,B:Type]. uiff(strong-subtype(A;B);(A \msubseteq{}r B) \mwedge{} respects-equality(B;A))
Date html generated:
2019_06_20-PM-00_27_50
Last ObjectModification:
2018_11_23-PM-00_21_55
Theory : subtype_1
Home
Index