# [Agda] lib solve f(x) = a

Twan van Laarhoven twanvl at gmail.com
Thu Jan 24 11:40:45 CET 2013

```On 24/01/13 11:32, Serge D. Mechveliani wrote:
> 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

That noSolution constructor just says that a given x is not a solution, it
doesn't say that there are no solutions. I would use

open import Data.Product      -- for ∃
open import Relation.Nullary  -- for Dec

Solution : {A B : Set} -> (f : A -> B) -> B -> Set
Solution f b = ∃ (\a -> f a ≡ b)

DecSolution : {A B : Set} -> (f : A -> B) -> B -> Set
DecSolution f b = Dec (Solution f b)

Or without the synonyms,

solve : ... (f : A -> B) -> (b : B) -> Dec (∃ (\a -> f a ≡ b))

Twan
```