Re: [Agda] Function.Equivalence._⇔_

[Andrés Sicard-Ramírez]

On 24 October 2013 14:15, Sergei Meshveliani <mechvel at botik.ru> wrote:

> I manage to build a value in  A ⇔ B  by applying the function
>  Equiv.equivalence.
> But, for example, having
>                   e  :  m≤n ⇔ suc-m≤suc-n
>
> how to extract    to :  m ≤ n → suc m ≤ suc n
> from  e  ?
>

Using auto (C-c C-a) I got:

open import Function.Equivalence
open import Function.Equality

foo : {A B : Set} → A ⇔ B → A → B
foo h = _⟨$⟩_ (Equivalence.to h)

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131024/82db6196/attachment.html