From d14c744a1cff323f8a837ef620a93ee518c392a2 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Thu, 7 May 2026 10:06:51 +0100
Subject: finish the implementation, we don't have motives so this is how it
 will have to stay

---
 examples/equality.makkai | 42 ++++++++++++++++++++++++------------------
 1 file changed, 24 insertions(+), 18 deletions(-)

(limited to 'examples')

diff --git a/examples/equality.makkai b/examples/equality.makkai
index ac668c7..5e9a0f9 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -2,31 +2,37 @@ let set Empty = variant[]
 let set Unit = record {}
 let element pt : Unit = {}
 
-let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
+let set Two = variant [ zero : Unit | one : Unit]
 
 let signature SetWithEquivRelation = theory {
     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)>
+    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 y z))
+                    -> <set-of(Relation x z)>
 
 }
-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 ] ],
-  .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)),
-                case x of [ zero. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
-                          | one.  z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
-                          | two.  z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
-                          ],
-  .Transitive = for (x: Three)(y: Three)(z: Three)(r: set-of(Relation x y))(s: set-of(Relation y z)), <pt>
+let instance eqTwo :: SetWithEquivRelation = {
+  .Carrier = Two :: Set,
+  .Relation = for (x: Two) (y: Two),
+                case x of [ zero. _ => case y of [ zero. _ => Unit  :: Set | one. _ => Empty :: Set ]
+                          | one.  _ => case y of [ zero. _ => Empty :: Set | one. _ => Unit  :: Set ] ],
+  .Reflexive = for (x: Two), case x of [ zero. _ => <pt> | one. _ => <pt> ],
+  .Symmetric = for (x: Two) (y: Two) (r: set-of(Relation x y)),
+                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
+                                 [ zero. _ => case z of [ zero. _ => <r> | one. _ => <s> ]
+                                 | one.  _ => case z of [ zero. _ => <pt>| one. _ => <r> ] ]
+                          | one.  _ => case y of
+                                 [ zero. _ => case z of [ zero. _ => <r> | one. _ => <pt>]
+                                 | one.  _ => case z of [ zero. _ => <s> | one. _ => <r> ] ] ]
 }
 
-// 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(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 }
+let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
-- 
cgit v1.3.1