diff options
Diffstat (limited to 'examples/equality.makkai')
| -rw-r--r-- | examples/equality.makkai | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/examples/equality.makkai b/examples/equality.makkai index a9b3368..ede2a54 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -4,16 +4,19 @@ let element pt : Unit = {} let set Three = variant [ zero : Unit | one : Unit | two : Unit ] -let signature EqS = (x : Three) (y: Three) -> theory { E :: Set } -let instance eqThree :: EqS = for (x: Three) (y: Three), { - .E = 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 ] - ] +let signature SetWitRelation = theory { + Carrier :: Set, + Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set + +} +let instance eqThree :: SetWitRelation = { + .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 ] ] } -let set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) } +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 oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt } |