Nuprl Definition : W

A parameterized family of W types with the parameter type Unit
must have the "C" function ⌜λp,a,b. ⋅⌝.
Then applying this family to the paramter ⌜⋅⌝, we get the W-type
as an instance of the more general parameterized family of types.⋅

W(A;a.B[a]) == pW ⋅

Definitions occuring in Statement : param-W: pW, it: ⋅, unit: Unit, apply: f a
Definitions occuring in definition : apply: f a, param-W: pW, unit: Unit, it: ⋅
FDL editor aliases : W

Latex:
W(A;a.B[a]) == pW \mcdot{} Date html generated: 2016_07_08-PM-04_47_47 Last ObjectModification: 2015_09_22-PM-05_47_16 Theory : co-recursion Home Index