### Nuprl Lemma : dep-fun-equiv-rel

`∀[X:Type]. ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ].`
`  ((∀x:X. EquivRel(A[x];a,b.E[x;a;b])) `` EquivRel(x:X ⟶ A[x];f,g.dep-fun-equiv(X;x,a,b.E[x;a;b];f;g)))`

Proof

Definitions occuring in Statement :  dep-fun-equiv: `dep-fun-equiv(X;x,a,b.E[x; a; b];f;g)` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2;s3]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` dep-fun-equiv: `dep-fun-equiv(X;x,a,b.E[x; a; b];f;g)` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` member: `t ∈ T` so_apply: `x[s]` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` so_apply: `x[s1;s2;s3]` subtype_rel: `A ⊆r B` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` guard: `{T}`
Lemmas referenced :  subtype_rel_self equiv_rel_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  independent_pairFormation sqequalRule because_Cache Error :functionIsType,  Error :universeIsType,  applyEquality hypothesisEquality cut hypothesis thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination Error :lambdaEquality_alt,  Error :inhabitedIsType,  universeEquality dependent_functionElimination productElimination independent_functionElimination

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{}  EquivRel(x:X  {}\mrightarrow{}  A[x];f,g.dep-fun-equiv(X;x,a,b.E[x;a;b];f;g)))

Date html generated: 2019_06_20-PM-00_32_56
Last ObjectModification: 2019_03_19-AM-10_42_34

Theory : quot_1

Home Index