[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Sat, 2018-11-17 at 16:54 +0000, Peter Hancock wrote:
> 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? 
> 
> [..]

Coercion has not sense in general. 
But mathematicians (S.Lang and Van der Waerden, and many others) write
that a group homomorphism is a map f that satisfies
the equality                            
                               f(xy) = f(x)f(y),

that a ring homomorphism needs to satisfy

                               f(x+y) = f(x) + f(y),
and so on.
These books write so, because this way it is easier to explain and to
understand. This has been tested by thousands of professors and millions
of students.

Generally, compilers are forced to follow science (mathematics). 

* For example, in early days programs used numbers instead of names. 
Then they have improved.
* They used different functions to add polynomials over integers, 
to add polynomials over rationals, over polynomial, and so on. 
Then, they have improved, and introduced generic programming -- this
follows mathematics.
* In mathematics, domains depend on a value, and this value can be
computed dynamically, and a function can return a domain.
Compilers could not handle this.
But they have improved, and now they can.  

* Similar it is (or will be) with implicit conversion.

Science has more sense than programming, science is wiser than a
technology, it is fundamental. And programming has to follow science.   

Regards,

------
Sergei