Nuprl Definition : param-co-W

The co-recursive family of parameterized co-W types.
For a given parameter p, a member w of ⌜pco-W p⌝ will be
a pair ⌜<a, f>⌝ where ⌜a ∈ A[p]⌝ and f is a function with
domain ⌜B[p; a]⌝. For b in the domain of f, ⌜f b⌝ is a member
of the co-W type in family that has parameter ⌜C[p; a; b]⌝.⋅

pco-W == corec-family(λW,p. (a:A[p] × (b:B[p; a] ⟶ (W C[p; a; b]))))

Definitions occuring in Statement : corec-family: corec-family(H), apply: f a, lambda: λx.A[x], function: x:A ⟶ B[x], product: x:A × B[x]
Definitions occuring in definition : corec-family: corec-family(H), lambda: λx.A[x], product: x:A × B[x], function: x:A ⟶ B[x], apply: f a
FDL editor aliases : param-co-W

Latex:
pco-W == corec-family(\mlambda{}W,p. (a:A[p] \mtimes{} (b:B[p; a] {}\mrightarrow{} (W C[p; a; b])))) Date html generated: 2016_07_08-PM-04_47_38 Last ObjectModification: 2015_09_22-PM-05_47_00 Theory : co-recursion Home Index