Nuprl Definition : fun-ss

A ⟶ ss ==
Point=A ⟶ Point(ss) #=λf,g. fun-sep(ss;A;f;g) cotrans=λf,g,h,fsep. let a,sep = fsep

                                                                  in case ss."#or" (f a) (g a) (h a) sep

                                                                      of inl(x) =>

                                                                      inl <a, x>

                                                                      | inr(y) =>

                                                                      inr <a, y>

Definitions occuring in Statement : fun-sep: fun-sep(ss;A;f;g), mk-ss: Point=P #=Sep cotrans=C, ss-point: Point(ss), apply: f a, lambda: λx.A[x], function: x:A ⟶ B[x], spread: spread def, pair: <a, b>, decide: case b of inl(x) => s[x] | inr(y) => t[y], inr: inr x , inl: inl x, token: "$token", record-select: r.x
Definitions occuring in definition : mk-ss: Point=P #=Sep cotrans=C, function: x:A ⟶ B[x], ss-point: Point(ss), fun-sep: fun-sep(ss;A;f;g), lambda: λx.A[x], spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y], record-select: r.x, token: "$token", apply: f a, inl: inl x, inr: inr x , pair: <a, b>
FDL editor aliases : fun-ss

Latex:
A {}\mrightarrow{} ss == Point=A {}\mrightarrow{} Point(ss) \#=\mlambda{}f,g. fun-sep(ss;A;f;g) cotrans=\mlambda{}f,g,h,fsep. let a,sep = fsep in case ss."\#or" (f a) (g a) (h a) sep of inl(x) => inl <a, x> | inr(y) => inr <a, y> Date html generated: 2019_10_31-AM-07_26_38 Last ObjectModification: 2019_09_19-PM-04_08_40 Theory : constructive!algebra Home Index