[Agda] I want implicit coercions in Agda

[Martin Escardo]

... and I am sure many other people do too.

Many other proof assistants have them.

Is there a philosophical reason for that, or is this something that just 
hasn't been done yet?

Real-life mathematics has them in abundance, and it would be nice to 
reflect this in Agda.

I would like to press for a design and implementation of this in Agda. :-)

Best,
Martin