Nuprl Lemma : fix_wf_corec-family-partial1
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. ∀[A:Type].
(∀[f:⋂T:P ⟶ Type. ((i:P ⟶ (T i) ⟶ partial(A)) ⟶ i:P ⟶ (H[T] i) ⟶ partial(A))]
(fix(f) ∈ i:P ⟶ (corec-family(H) i) ⟶ partial(A))) supposing
((family-monotone{i:l}(P;H) ∧ type-family-continuous{i:l}(P;H)) and
mono(A) and
value-type(A))
Proof
Definitions occuring in Statement :
corec-family: corec-family(H),
type-family-continuous: type-family-continuous{i:l}(P;H),
family-monotone: family-monotone{i:l}(P;H),
partial: partial(T),
mono: mono(T),
value-type: value-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
and: P ∧ Q,
member: t ∈ T,
apply: f a,
fix: fix(F),
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
so_apply: x[s],
prop: ℙ,
cand: A c∧ B,
subtype_rel: A ⊆r B,
ext-family: F ≡ G,
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
ext-eq: A ≡ B,
istype: istype(T)
Lemmas referenced :
partial_wf,
family-monotone_wf,
type-family-continuous_wf,
mono_wf,
value-type_wf,
istype-universe,
corec-family-ext,
corec-family_wf,
subtype_rel_dep_function,
fix-corec-family-partial1
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
hypothesis,
sqequalRule,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
Error :isectIsType,
Error :functionIsType,
Error :universeIsType,
hypothesisEquality,
Error :inhabitedIsType,
because_Cache,
applyEquality,
extract_by_obid,
isectElimination,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies,
Error :productIsType,
instantiate,
universeEquality,
independent_isectElimination,
independent_pairFormation,
Error :lambdaEquality_alt,
functionExtensionality,
dependent_functionElimination,
Error :lambdaFormation_alt,
functionEquality
Latex:
\mforall{}[P:Type]. \mforall{}[H:(P {}\mrightarrow{} Type) {}\mrightarrow{} P {}\mrightarrow{} Type]. \mforall{}[A:Type].
(\mforall{}[f:\mcap{}T:P {}\mrightarrow{} Type. ((i:P {}\mrightarrow{} (T i) {}\mrightarrow{} partial(A)) {}\mrightarrow{} i:P {}\mrightarrow{} (H[T] i) {}\mrightarrow{} partial(A))]
(fix(f) \mmember{} i:P {}\mrightarrow{} (corec-family(H) i) {}\mrightarrow{} partial(A))) supposing
((family-monotone\{i:l\}(P;H) \mwedge{} type-family-continuous\{i:l\}(P;H)) and
mono(A) and
value-type(A))
Date html generated:
2019_06_20-PM-00_35_30
Last ObjectModification:
2019_02_20-PM-04_58_37
Theory : co-recursion
Home
Index