module exampleColourEquality where

data Bool : Set where
  tt : Bool
  ff : Bool


data ⊤ : Set where
  true : ⊤ 

data ⊥ : Set where

Atom : Bool -> Set
Atom tt = ⊤
Atom ff = ⊥ 

data Colour : Set where
  blue  : Colour
  red   : Colour
  green : Colour


eqColourBool : Colour -> Colour -> Bool
eqColourBool blue blue   = tt
eqColourBool red red     = tt
eqColourBool green green = tt
eqColourBool _  _        = tt

_==_ : Colour -> Colour -> Set
c == c' = Atom (eqColourBool c c')

_=='_ : Colour -> Colour -> Set
blue  ==' blue   = ⊤ 
red   ==' red    = ⊤ 
green ==' green  = ⊤ 
_     ==' _      = ⊥