add complete lifted sets

1 files changed, 27 insertions, 3 deletions

diff --git a/examples/equality.makkai b/examples/equality.makkai
index 5e9a0f9..86b81ae 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -1,9 +1,11 @@
+// basic prelude
 let set Empty = variant[]
 let set Unit = record {}
 let element pt : Unit = {}
-
+// Bool is not inductive
 let set Two = variant [ zero : Unit | one : Unit]
 
+// the main thrust
 let signature SetWithEquivRelation = theory {
     Carrier :: Set,
     Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set,
@@ -15,6 +17,8 @@ let signature SetWithEquivRelation = theory {
                     -> <set-of(Relation x z)>
 
 }
+
+// by cases we construct this on Two
 let instance eqTwo :: SetWithEquivRelation = {
   .Carrier = Two :: Set,
   .Relation = for (x: Two) (y: Two),
@@ -25,7 +29,7 @@ let instance eqTwo :: SetWithEquivRelation = {
                 case x of [ zero. _ => case y of [ zero. _ => <r> | one. _ => <r> ]
                           | one.  _ => case y of [ zero. _ => <r> | one. _ => <r> ] ],
   .Transitive = for (x: Two)(y: Two)(z: Two)(r: set-of(Relation x y))(s: set-of(Relation y z)),
-                case x of [ zero. _ => case y of
+                case x of [ zero. _ => case y of // there are choices here to use <r> or <s> in places that are irrelevant
                                  [ zero. _ => case z of [ zero. _ => <r> | one. _ => <s> ]
                                  | one.  _ => case z of [ zero. _ => <pt>| one. _ => <r> ] ]
                           | one.  _ => case y of
@@ -33,6 +37,26 @@ let instance eqTwo :: SetWithEquivRelation = {
                                  | one.  _ => case z of [ zero. _ => <s> | one. _ => <r> ] ] ]
 }
 
+// show off forming sets
 let set Diagonal = record { x : set-of(eqTwo .Carrier), y : set-of(eqTwo .Carrier), equal : set-of((eqTwo .Relation) x y) }
-
 let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
+
+// prove inequality
+let instance zeroNeqOne
+    :: (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))) -> <Empty>
+    = for (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))), <r>
+
+// prove inequality the fun way
+let signature NeqParticular = theory {
+    SE :: SetWithEquivRelation,
+    A :: <set-of(SE .Carrier)>,
+    B :: <set-of(SE .Carrier)>,
+    Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty>
+}
+
+let instance zeroNeqOne :: NeqParticular = {
+    .SE = eqTwo,
+    .A = <zero. pt>,
+    .B = <one. pt>,
+    .Neq = for (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))), <r>
+}