[Agda] lib solve f(x) = a
Twan van Laarhoven
twanvl at gmail.com
Thu Jan 24 12:51:37 CET 2013
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.
More information about the Agda