diff options
Diffstat (limited to 'examples/equality.makkai')
| -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> } |