diff options
| author | tslil <tslil@posteo.de> | 2026-05-06 20:43:00 +0100 |
|---|---|---|
| committer | tslil <tslil@posteo.de> | 2026-05-06 22:42:00 +0100 |
| commit | fb5ba7fb62f4ce75f307233d5ffb438243f353b6 (patch) | |
| tree | 35b489025f7accfb73e40e2d8dad46ef1b4f2963 /examples | |
| parent | d682ad6bbb5547ffbcc19da90275ff43e4e03e20 (diff) | |
fixing ...
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/equality.makkai | 6 |
1 files changed, 5 insertions, 1 deletions
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> } |