structural ability Either a b where
  left : a -> {Either a b} ()
  right : b -> {Either a b} ()

structural type Either a b = Left a | Right b