Nuprl Lemma : type-function-eta
∀[A:Type]. ∀[B,C:type-function{i:l}(A)].
((B = C ∈ type-function{i:l}(A)) ⇒ ((λx.(B x)) = (λx.(C x)) ∈ type-function{i:l}(A)))
Proof
Definitions occuring in Statement :
type-function: type-function{i:l}(A),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
apply: f a,
lambda: λx.A[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
type-function: type-function{i:l}(A),
member: t ∈ T,
per-function: per-function(A;a.B[a]),
function-eq: function-eq(A;a.B[a];f;g),
uimplies: b supposing a,
tf-apply: tf-apply(f;x),
squash: ↓T,
guard: {T},
true: True,
prop: ℙ,
subtype_rel: A ⊆r B
Lemmas referenced :
type-function_wf,
per-function_wf_type,
tf-apply_wf,
subtype_rel_self,
equal_functionality_wrt_subtype_rel2,
equal_wf,
squash_wf,
true_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaFormation_alt,
sqequalHypSubstitution,
Error :equalityIsType1,
Error :inhabitedIsType,
hypothesisEquality,
Error :universeIsType,
cut,
introduction,
extract_by_obid,
isectElimination,
thin,
hypothesis,
universeEquality,
pointwiseFunctionality,
sqequalRule,
pertypeMemberEquality,
rename,
equalityTransitivity,
equalitySymmetry,
applyEquality,
Error :lambdaEquality_alt,
imageElimination,
because_Cache,
instantiate,
independent_isectElimination,
independent_functionElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
Error :equalityIsType4,
Error :isect_memberEquality_alt,
axiomEquality,
baseApply,
closedConclusion
Latex:
\mforall{}[A:Type]. \mforall{}[B,C:type-function\{i:l\}(A)]. ((B = C) {}\mRightarrow{} ((\mlambda{}x.(B x)) = (\mlambda{}x.(C x))))
Date html generated:
2019_06_20-AM-11_30_02
Last ObjectModification:
2018_09_28-PM-11_21_21
Theory : per!type
Home
Index