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