equal
deleted
inserted
replaced
17 Pair_Rep :: ['a, 'b] => ['a, 'b] => bool |
17 Pair_Rep :: ['a, 'b] => ['a, 'b] => bool |
18 |
18 |
19 defs |
19 defs |
20 Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)" |
20 Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)" |
21 |
21 |
22 subtype (Prod) |
22 typedef (Prod) |
23 ('a, 'b) "*" (infixr 20) |
23 ('a, 'b) "*" (infixr 20) |
24 = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}" |
24 = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}" |
25 |
25 |
26 |
26 |
27 (* abstract constants and syntax *) |
27 (* abstract constants and syntax *) |
59 prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" |
59 prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" |
60 Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" |
60 Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" |
61 |
61 |
62 (** Unit **) |
62 (** Unit **) |
63 |
63 |
64 subtype (Unit) |
64 typedef (Unit) |
65 unit = "{p. p = True}" |
65 unit = "{p. p = True}" |
66 |
66 |
67 consts |
67 consts |
68 "()" :: unit ("'(')") |
68 "()" :: unit ("'(')") |
69 |
69 |