[Agda] I want implicit coercions in Agda

[Martin Escardo]

On 17/11/2018 16:32, jon at jonmsterling.com wrote:
> the boundary between sensible overloading and perverse overloading is a very fine one, and rarely do mathematical texts actually walk that boundary in a satisfactory way.

Indeed, it is an art to write mathematics well (or to write anything at 
all well). Most people don't.

It would be very surprising if legislation by the proof-assistant 
community would elevate mathematical writing to the levels of, say, Gian 
Carlo Rota.

Please let the proof assistants have the modes of expression that 
mathematicians do use in practice, and the mathematical community to 
judge (as it has done for centuries and millennia) the qualities of the 
writings of each mathematician.

You will not solve the shortcomings of my mathematical style by refusing 
to implement implicit coercion in Agda.

Best,
Martin