Nuprl Lemma : dep-fun-equiv_wf
∀[X:Type]. ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ]. ∀[f,g:x:X ⟶ A[x]]. (dep-fun-equiv(X;x,f,g.E[x;f;g];f;g) ∈ ℙ)
Proof
Definitions occuring in Statement :
dep-fun-equiv: dep-fun-equiv(X;x,a,b.E[x; a; b];f;g),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3],
so_apply: x[s],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
prop: ℙ,
so_apply: x[s],
so_apply: x[s1;s2;s3],
so_lambda: λ2x.t[x],
dep-fun-equiv: dep-fun-equiv(X;x,a,b.E[x; a; b];f;g),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
all_wf
Rules used in proof :
universeEquality,
because_Cache,
isect_memberEquality,
functionEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
hypothesis,
functionExtensionality,
applyEquality,
lambdaEquality,
hypothesisEquality,
cumulativity,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[X:Type]. \mforall{}[A:X {}\mrightarrow{} Type]. \mforall{}[E:x:X {}\mrightarrow{} A[x] {}\mrightarrow{} A[x] {}\mrightarrow{} \mBbbP{}]. \mforall{}[f,g:x:X {}\mrightarrow{} A[x]].
(dep-fun-equiv(X;x,f,g.E[x;f;g];f;g) \mmember{} \mBbbP{})
Date html generated:
2017_09_29-PM-05_48_14
Last ObjectModification:
2017_09_07-PM-03_21_44
Theory : quot_1
Home
Index