[Agda] I want implicit coercions in Agda

[Peter Hancock]

On 17/11/2018 15:53, Martin Escardo wrote:
> If you want mathematicians to use proof assistants, you have to
> implement the notations they use, not the notations that computer
> scientists / engineers find convenient to write computer programs.
> Martin

You might as well say that if you want mathematicians to use 
type-setting software you have to implement the notations they use.
The mathematicians I know seem to find their way pretty well around LaTeX, etc,
for all its barbarity. 

Perhaps one can think of mathematical notation as a matter of DSLs.
LaTeX is full of DSL-like apparatus for things like category theory diagrams, etc.
I think the support in Agda for equational reasoning might be
a nice example of a DSL.

Is there a general definition of coercion?  Is there a connection with identity types? 

Is changing coordinates from Cartesian to Polar something a coercion might do?