[Agda] lib solve f(x) = a

[Twan van Laarhoven]

On 24/01/13 12:20, Serge D. Mechveliani wrote:
> On Thu, Jan 24, 2013 at 11:40:45AM +0100, Twan van Laarhoven wrote:
>> Or without the synonyms,
>>
>>      solve : ... (f : A -> B) -> (b : B) -> Dec (\exists (\a -> f a ~~ b))
>>
>
> This latter line looks the best -- if only  \exists  means the needed
> constructive thing (I need to look into  \exists).

It does. ∃ is defined as

     ∃ = Σ _

and Σ is a dependent sum, i.e. a record with two fields. All ∃ does extra is to 
infer the first argument, `A` in this case.



Twan