From fb5ba7fb62f4ce75f307233d5ffb438243f353b6 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Wed, 6 May 2026 20:43:00 +0100
Subject: fixing ...

---
 examples/equality.makkai | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'examples/equality.makkai')

diff --git a/examples/equality.makkai b/examples/equality.makkai
index 438e930..ac668c7 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -19,7 +19,11 @@ let instance eqThree :: SetWithEquivRelation = {
                           | 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)), <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>
 }
 
-- 
cgit v1.3.1