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 Error :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 : coW-wfdd: coW-wfdd(a.B[a];w), coW: coW(A;a.B[a]), set: {x:A| B[x]}
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: 2018_07_29-AM-09_21_58 Last ObjectModification: 2018_07_26-PM-09_22_28 Theory : co-recursion Home Index