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