Nuprl Lemma : co-regext-loopset
Now we do get ⌜(loopset() ⊆ co-regext(loopset()))⌝, because the type
⌜coW(Unit;x.Unit)⌝ has a single member (while the corresponding W type
⌜W(Unit;x.Unit)⌝ is empty). So the needed property
⌜∀a:coSet{i:l}. (transitive-set(a) ⇒ (a ⊆ co-regext(a)))⌝ could be true??..⋅
seteq(co-regext(loopset());loopset())
Proof
Definitions occuring in Statement :
co-regext: co-regext(a),
loopset: loopset(),
seteq: seteq(s1;s2)
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
loopset: loopset(),
set-dom: set-dom(s),
pi1: fst(t),
guard: {T},
implies: P ⇒ Q,
and: P ∧ Q,
uimplies: b supposing a,
respects-equality: respects-equality(S;T),
subtype_rel: A ⊆r B,
regextfun: regextfun(f;w),
mk-coset: mk-coset(T;f),
mk-set: f"(T),
Wsup: Wsup(a;b),
ext-eq: A ≡ B,
unit: Unit,
prop: ℙ,
so_apply: x[s1;s2],
F-bisimulation: x,y.R[x; y] is an T.F[T]-bisimulation,
true: True,
squash: ↓T,
exists: ∃x:A. B[x],
top: Top,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
co-regext: co-regext(a)
Lemmas referenced :
regextfun_wf,
unit_wf2,
loopset_wf,
coW_wf,
coSet-equality2,
subtype_rel_wf,
coSet_wf,
istype-universe,
subtype-respects-equality,
loopset-sq,
coW-ext,
subtype_rel_weakening,
equal-wf-base,
set-dom_wf,
coW-corec,
ext-eq_inversion,
corec_wf,
coinduction-principle,
continuous-monotone-product,
continuous-monotone-constant,
continuous-monotone-function,
continuous-monotone-id,
true_wf,
istype-true,
corec-ext,
equal-unit,
subtype_rel_self,
iff_wf,
all_wf,
setmem-loopset,
exists_wf,
setmem_wf,
iff_weakening_equal,
squash_wf,
seteq_wf,
setmem-mk-coset,
co-regext_wf,
co-seteq-iff,
fix_wf_coW,
it_wf,
fix_wf_corec
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
lambdaEquality,
sqequalRule,
hypothesisEquality,
lambdaFormation_alt,
universeIsType,
lambdaEquality_alt,
dependent_functionElimination,
independent_functionElimination,
productIsType,
instantiate,
productEquality,
universeEquality,
functionEquality,
cumulativity,
productElimination,
equalityIstype,
baseClosed,
independent_isectElimination,
sqequalBase,
equalitySymmetry,
hypothesis_subsumption,
applyEquality,
because_Cache,
inhabitedIsType,
dependent_pairEquality_alt,
functionIsType,
intEquality,
equalityTransitivity,
promote_hyp,
natural_numberEquality,
functionExtensionality_alt,
applyLambdaEquality,
impliesFunctionality,
allFunctionality,
addLevel,
imageMemberEquality,
imageElimination,
voidEquality,
voidElimination,
isect_memberEquality,
independent_pairFormation,
dependent_pairEquality,
rename,
dependent_pairFormation
Latex:
seteq(co-regext(loopset());loopset())
Date html generated:
2020_05_20-PM-01_19_29
Last ObjectModification:
2019_12_10-AM-11_33_32
Theory : constructive!set!theory
Home
Index