data Maybe {a} (A : Set a) : Set a where
  just    : (x : A) !$\rightarrow$! Maybe A
  nothing : Maybe A