Nuprl Definition : W-type
W-type(A; a.B[a]) == {w:co-W(A;a.B[a])| ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(w;p)}
Definitions occuring in Statement :
W-bars: W-bars(w;p),
co-W: co-W(A;a.B[a]),
nat: ℕ,
all: ∀x:A. B[x],
unit: Unit,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
union: left + right
Definitions occuring in definition :
set: {x:A| B[x]} ,
co-W: co-W(A;a.B[a]),
all: ∀x:A. B[x],
nat: ℕ,
function: x:A ⟶ B[x],
union: left + right,
unit: Unit,
W-bars: W-bars(w;p)
Latex:
W-type(A; a.B[a]) == \{w:co-W(A;a.B[a])| \mforall{}p:\mBbbN{} {}\mrightarrow{} a:A {}\mrightarrow{} (B[a]?). W-bars(w;p)\}
Date html generated:
2016_05_15-PM-10_06_47
Last ObjectModification:
2015_09_23-AM-08_22_17
Theory : bar!induction
Home
Index