Nuprl Definition : altW

We defined the W-type as a special case of the parameterized family
of W-types, so the proof of the induction principle is somewhat
complicated.  Here we give an alternate definition as the
subtype of w ∈ coW(A;a.B[a]) for which ⌜coW-wfdd(a.B[a];w)⌝.

Then the induction operator is
altWind(h;w) ==  h w (λb.altWind(h;coW-item(w;b)))
and we directly prove that altWind(h;w) witnesses the induction
principle for altW(A;a.B[a])  by using bar induction
(see altWind_wf)⋅

altW(A;a.B[a]) == {w:coW(A;a.B[a])| coW-wfdd(a.B[a];w)}

Definitions occuring in Statement : coW-wfdd: coW-wfdd(a.B[a];w), coW: coW(A;a.B[a]), set: {x:A| B[x]}
Definitions occuring in definition : set: {x:A| B[x]} , coW: coW(A;a.B[a]), coW-wfdd: coW-wfdd(a.B[a];w)
FDL editor aliases : altW

Latex:
altW(A;a.B[a]) == \{w:coW(A;a.B[a])| coW-wfdd(a.B[a];w)\} Date html generated: 2019_06_20-PM-01_12_11 Last ObjectModification: 2019_01_02-PM-01_35_41 Theory : co-recursion-2 Home Index