Nuprl Lemma : all-quotient
∀T:Type
(canonicalizable(T)
⇒ (∀S:Type. ∀E:S ⟶ S ⟶ ℙ.
(EquivRel(S;a,b.E[a;b]) ⇒ (∀t:T. (x,y:S//E[x;y]) ⇐⇒ f,g:∀t:T. S//fun-equiv(T;a,b.↓E[a;b];f;g)))))
Proof
Definitions occuring in Statement :
fun-equiv: fun-equiv(X;a,b.E[a; b];f;g),
equiv_rel: EquivRel(T;x,y.E[x; y]),
quotient: x,y:A//B[x; y],
canonicalizable: canonicalizable(T),
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
squash: ↓T,
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
prop: ℙ,
so_apply: x[s],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
iff: P ⇐⇒ Q,
and: P ∧ Q,
fun-equiv: fun-equiv(X;a,b.E[a; b];f;g),
dep-fun-equiv: dep-fun-equiv(X;x,a,b.E[x; a; b];f;g),
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_lambda: λ2x y.t[x; y],
uimplies: b supposing a,
rev_implies: P ⇐ Q
Lemmas referenced :
all-quotient-dependent,
all_wf,
quotient_wf,
fun-equiv_wf,
squash_wf,
fun-equiv-rel,
equiv_rel_squash,
equiv_rel_wf,
canonicalizable_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
lambdaEquality,
sqequalRule,
cumulativity,
productElimination,
independent_pairFormation,
isectElimination,
applyEquality,
functionExtensionality,
independent_isectElimination,
because_Cache,
functionEquality,
universeEquality
Latex:
\mforall{}T:Type
(canonicalizable(T)
{}\mRightarrow{} (\mforall{}S:Type. \mforall{}E:S {}\mrightarrow{} S {}\mrightarrow{} \mBbbP{}.
(EquivRel(S;a,b.E[a;b])
{}\mRightarrow{} (\mforall{}t:T. (x,y:S//E[x;y]) \mLeftarrow{}{}\mRightarrow{} f,g:\mforall{}t:T. S//fun-equiv(T;a,b.\mdownarrow{}E[a;b];f;g)))))
Date html generated:
2018_05_21-PM-01_20_10
Last ObjectModification:
2017_11_03-PM-02_33_17
Theory : continuity
Home
Index