[Agda] I want implicit coercions in Agda

[Martin Escardo]

On 18/11/2018 20:35, ulf.norell at gmail.com wrote:
> On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo <m.escardo at cs.bham.ac.uk 
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
> 
>     You will not solve the shortcomings of my mathematical style by
>     refusing
>     to implement implicit coercion in Agda.
> 
> 
> I feel that the discussion has derailed a little at this point. The 
> issue isn't that some people
> are stubbornly refusing to implement this 

This reply was not directed to the Agda developers, but instead to the 
people who ranted against these features.

I will be happy to give a list of things for which implicit coercions 
are used by mathematicians, including those of my own Agda developments.

Martin