### 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