clean up examples vs tests

8 files changed, 12 insertions, 11 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 }
diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai
index 590cf04..f7e7bff 100644
--- a/examples/one_simplex.makkai
+++ b/examples/one_simplex.makkai
@@ -6,8 +6,6 @@ let signature Graph = theory {
 let set Empty = variant[]
 let set Unit = record{}
 let element pt : Unit = {}
-let set F1 = variant [ one0 : Unit ]
-let set F2 = variant [ two0 : Unit | two1 : Unit ]
 let set F3 = variant [ three0 : Unit | three1 : Unit  | three2: Unit ]
 
 let instance oneSimplex :: Graph = {
diff --git a/examples/alpha_equiv.makkai b/examples/tests/test_alpha_equiv.makkai
index 2ae067a..2ae067a 100644
--- a/examples/alpha_equiv.makkai
+++ b/examples/tests/test_alpha_equiv.makkai
diff --git a/examples/ext_codomain.makkai b/examples/tests/test_ext_codomain.makkai
index da0ddae..da0ddae 100644
--- a/examples/ext_codomain.makkai
+++ b/examples/tests/test_ext_codomain.makkai
diff --git a/examples/inline_nested.makkai b/examples/tests/test_inline_nested.makkai
index e891349..e891349 100644
--- a/examples/inline_nested.makkai
+++ b/examples/tests/test_inline_nested.makkai
diff --git a/examples/nested_for.makkai b/examples/tests/test_nested_for.makkai
index b3618cc..b3618cc 100644
--- a/examples/nested_for.makkai
+++ b/examples/tests/test_nested_for.makkai
diff --git a/examples/signature_merge.makkai b/examples/tests/test_signature_merge.makkai
index 5f575d5..5f575d5 100644
--- a/examples/signature_merge.makkai
+++ b/examples/tests/test_signature_merge.makkai
diff --git a/examples/signature_param.makkai b/examples/tests/test_signature_param.makkai
index 9dae31b..9dae31b 100644
--- a/examples/signature_param.makkai
+++ b/examples/tests/test_signature_param.makkai