### Nuprl Lemma : quotient-dep-function-subtype

`∀[X:Type]`
`  ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ].`
`    ((∀x:X. EquivRel(A[x];a,b.E[x;a;b]))`
`    `` ((x:X ⟶ (a,b:A[x]//E[x;a;b])) ⊆r (f,g:x:X ⟶ A[x]//(∀x:X. (↓E[x;f x;g x]))))) `
`  supposing X ⊆r Base`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2;s3]` so_apply: `x[s]` all: `∀x:A. B[x]` squash: `↓T` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` base: `Base` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` implies: `P `` Q` all: `∀x:A. B[x]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2;s3]` so_apply: `x[s1;s2]` prop: `ℙ` subtype_rel: `A ⊆r B` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` squash: `↓T` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` guard: `{T}` bfalse: `ff` ext-eq: `A ≡ B` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` isect2: `T1 ⋂ T2` so_lambda: `λ2x.t[x]` true: `True` quotient: `x,y:A//B[x; y]`
Lemmas referenced :  quotient-squash equiv_rel_squash equiv_rel_wf subtype_rel_wf base_wf istype-universe squash_wf quotient_wf subtype_rel_weakening isect2_wf subtype_rel_transitivity isect2_subtype_rel quotient-isect-base void_wf all_wf quotient-member-eq member_wf true_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality sqequalRule Error :lambdaEquality_alt,  Error :inhabitedIsType,  Error :universeIsType,  because_Cache independent_isectElimination hypothesis dependent_functionElimination independent_functionElimination Error :functionIsType,  axiomEquality Error :functionIsTypeImplies,  universeEquality Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  instantiate independent_pairFormation imageMemberEquality baseClosed imageElimination productElimination Error :equalityIstype,  equalityTransitivity equalitySymmetry pointwiseFunctionality closedConclusion baseApply Error :equalityIsType1,  equalityElimination unionElimination isect_memberEquality Error :functionExtensionality_alt,  voidElimination functionExtensionality functionEquality natural_numberEquality applyLambdaEquality pertypeElimination promote_hyp Error :productIsType,  sqequalBase

Latex:
\mforall{}[X:Type]
\mforall{}[A:X  {}\mrightarrow{}  Type].  \mforall{}[E:x:X  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x:X.  EquivRel(A[x];a,b.E[x;a;b]))
{}\mRightarrow{}  ((x:X  {}\mrightarrow{}  (a,b:A[x]//E[x;a;b]))  \msubseteq{}r  (f,g:x:X  {}\mrightarrow{}  A[x]//(\mforall{}x:X.  (\mdownarrow{}E[x;f  x;g  x])))))
supposing  X  \msubseteq{}r  Base

Date html generated: 2019_06_20-PM-00_32_33
Last ObjectModification: 2018_11_26-AM-00_13_30

Theory : quot_1

Home Index