Nuprl Definition : co-W
co-W(A;a.B[a]) == corec(T.a:A × (B[a] ⟶ T))
Definitions occuring in Statement :
corec: corec(T.F[T]),
function: x:A ⟶ B[x],
product: x:A × B[x]
Definitions occuring in definition :
corec: corec(T.F[T]),
product: x:A × B[x],
function: x:A ⟶ B[x]
FDL editor aliases :
co-W
Latex:
co-W(A;a.B[a]) == corec(T.a:A \mtimes{} (B[a] {}\mrightarrow{} T))
Date html generated:
2016_05_15-PM-10_06_26
Last ObjectModification:
2015_09_23-AM-08_22_15
Theory : bar!induction
Home
Index