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

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

let signature SetWithEquivRelation = theory {
    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 :: 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 ] ],
  .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)),
                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>
}

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