WiP

1 files changed, 12 insertions, 6 deletions

diff --git a/examples/equality.makkai b/examples/equality.makkai
index ede2a54..438e930 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -4,19 +4,25 @@ let element pt : Unit = {}
 
 let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
 
-let signature SetWitRelation = theory {
+let signature SetWithEquivRelation = theory {
     Carrier :: Set,
-    Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set
+    Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set,
+    Reflexive :: (x : set-of(Carrier)) -> <set-of(Relation x x)>,
+    Symmetric :: (x : set-of(Carrier)) (y : set-of(Carrier)) (r : set-of(Relation x y)) -> <set-of(Relation y x)>,
+    Transitive :: (x : set-of(Carrier)) (y : set-of(Carrier)) (z : set-of(Carrier)) (r : set-of(Relation x y)) (s : set-of(Relation z z)) -> <set-of(Relation y z)>
 
 }
-let instance eqThree :: SetWitRelation = {
+let instance eqThree :: SetWithEquivRelation = {
   .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 ] ]
+                          | two.  z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit  :: Set ] ],
+  .Reflexive = for (x: Three), case x of [ zero. z => <pt> | one. z => <pt> | two. z => <pt> ],
+  .Symmetric = for (x: Three)(y: Three)(r: set-of(Relation x y)), <pt>,
+  .Transitive = for (x: Three)(y: Three)(z: Three)(r: set-of(Relation x y))(s: set-of(Relation y z)), <pt>
 }
 
-let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) }
+// 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 oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }