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