clean up examples vs tests

1 files changed, 12 insertions, 9 deletions

diff --git a/examples/equality.makkai b/examples/equality.makkai
index a9b3368..ede2a54 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -4,16 +4,19 @@ let element pt : Unit = {}
 
 let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
 
-let signature EqS = (x : Three) (y: Three) -> theory { E :: Set }
-let instance eqThree :: EqS = for (x: Three) (y: Three), {
-    .E = case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ]
-                   | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ]
-                   | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ]
-                   ]
+let signature SetWitRelation = theory {
+    Carrier :: Set,
+    Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set
+
+}
+let instance eqThree :: SetWitRelation = {
+  .Carrier = Three :: Set,
+  .Relation = for (x: Three) (y: Three),
+                case x of [ zero. z => case y of [ zero. w => Unit  :: Set | one. w => Empty :: Set | two. w => Empty :: Set ]
+                          | one.  z => case y of [ zero. w => Empty :: Set | one. w => Unit  :: Set | two. w => Empty :: Set ]
+                          | two.  z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit  :: Set ] ]
 }
 
-let set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) }
+let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) }
 
 let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
-
-let element oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt }