examples/equality.makkai


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

let set Empty = variant[]
let set Unit = record {}
let element pt : Unit = {}

let set Three = variant [ zero : Unit | one : Unit | two : Unit ]

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 : 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 }