Nuprl Definition : corec-family

family of type parameterized by is member of
the type ⌜P ⟶ Type⌝.
The family of types ⌜λp.Top⌝ is the greatest such family
(under the pointwise subtype ordering).
If maps ⌜P ⟶ Type⌝ to ⌜P ⟶ Type⌝then the intersection (as family)
of the iterates of is the corecursive family defined by H.

If satisfies the properties ⌜type-family-continuous{i:l}(P;H)⌝
and ⌜family-monotone{i:l}(P;H)⌝then the ⌜corec-family(H)⌝ is an
extensional fixed point of H.
(See lemma corec-family-ext)⋅

corec-family(H) ==  ⋂n:ℕH^n p.Top)

Definitions occuring in Statement :  isect-family: a:A. F[a] fun_exp: f^n nat: top: Top apply: a lambda: λx.A[x]
Definitions occuring in definition :  isect-family: a:A. F[a] nat: apply: a fun_exp: f^n lambda: λx.A[x] top: Top
FDL editor aliases :  corec-family

corec-family(H)  ==    \mcap{}n:\mBbbN{}.  H\^{}n  (\mlambda{}p.Top)

Date html generated: 2016_07_08-PM-04_47_37
Last ObjectModification: 2015_09_22-PM-05_47_00

Theory : co-recursion

Home Index