Nuprl Definition : W_corec
This is a generalization of ⌜corec(T.F[T])⌝ where instead of iterating
only over the natural numbers, we iterate over all the "ordinals" in
the type ⌜W(A;a.B[a])⌝.⋅
W_corec(A;a.B[a];T.F[T]) == ⋂w:W(A;a.B[a]). W_iterate_functor(A;a.B[a];T.F[T];w)
Definitions occuring in Statement :
W_iterate_functor: W_iterate_functor(A;a.B[a];T.F[T];w),
W: W(A;a.B[a]),
isect: ⋂x:A. B[x]
Definitions occuring in definition :
isect: ⋂x:A. B[x],
W: W(A;a.B[a]),
W_iterate_functor: W_iterate_functor(A;a.B[a];T.F[T];w)
FDL editor aliases :
W_corec
Latex:
W\_corec(A;a.B[a];T.F[T]) == \mcap{}w:W(A;a.B[a]). W\_iterate\_functor(A;a.B[a];T.F[T];w)
Date html generated:
2016_07_08-PM-04_47_49
Last ObjectModification:
2015_09_22-PM-05_47_21
Theory : co-recursion
Home
Index