29 "QSUM x:A. B" => "QSigma(A, %x. B)" |
29 "QSUM x:A. B" => "QSigma(A, %x. B)" |
30 "A <*> B" => "QSigma(A, _K(B))" |
30 "A <*> B" => "QSigma(A, _K(B))" |
31 |
31 |
32 rules |
32 rules |
33 QPair_def "<a;b> == a+b" |
33 QPair_def "<a;b> == a+b" |
34 qsplit_def "qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b)" |
34 qsplit_def "qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b)" |
35 qfsplit_def "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)" |
35 qfsplit_def "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)" |
36 qconverse_def "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" |
36 qconverse_def "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" |
37 QSigma_def "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}" |
37 QSigma_def "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}" |
38 |
38 |
39 qsum_def "A <+> B == QSigma({0}, %x.A) Un QSigma({1}, %x.B)" |
39 qsum_def "A <+> B == ({0} <*> A) Un ({1} <*> B)" |
40 QInl_def "QInl(a) == <0;a>" |
40 QInl_def "QInl(a) == <0;a>" |
41 QInr_def "QInr(b) == <1;b>" |
41 QInr_def "QInr(b) == <1;b>" |
42 qcase_def "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
42 qcase_def "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
43 end |
43 end |
44 |
44 |