examples/equality.makkai


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

let set Empty = variant[]
let set Unit = record {}
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 set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) }

let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }

let element oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt }