[Agda] lib solve f(x) = a

[Serge D. Mechveliani]

People,
I need the signature for decidable solution for  f x = b,

           solve : ... (f : A -> B) -> (b : B) -> DecSolution f b  

(some details skipped)
-- any solution, with a proof, or a proof for the solution absence.

  record Solution ... (f : A -> B) (b : B)  : Set _  where
                                   field  
                                     solution : A
                                     proof    : (f solution) \~~ b
  data DecSolution ... f b : Set _
       where
       solved     : Solution f b                -> DecSolution f b
       noSolution : (x : A) -> \neg (f x \~~ a) -> DecSolution f b

I can define something like this as an user data.
But has Standard library some closely related item?

Thanks,
Sergei