[Agda] I want implicit coercions in Agda

[Peter Hancock]

On 18/11/2018 21:32, Jason -Zhong Sheng- Hu wrote:
> If we can have a hierarchy of views, which allows us to zoom in and
> out of mathematics/proofs/programs, I think coersion can have way
> more value.

Someone who's opinion is worth having about the presentation of
mathematical material is Lamport.  I am thinking about his
specification language TLA+, and  its proof system TLP (I think).

These formalisms were designed to be used by engineers, who I suppose
are mathematicians of some kind. Stylistically, they resemble COBOL,
with lots of upper-case keywords, etc.  IMHO, they are readable, largely
because notational fuss is kept to a minimum.  Things are designed to be
emailable in ASCII. 

Most interesting is that TLP is designed for writing informal proofs.
At any point, you can put in an informal "handwave" (a bit like a hole). 
A "folding" metaphor is used to browse TLP proofs. You can choose to
hide uninteresting portions of a proof, and drill down to 
particular steps in full gory detail.  Lamport says one should
write a proof in small enough steps that everything is completely obvious,
then provide one more level of formal proof.

I presume coercions are injective functions that resolve type-clashes between 
things like natural numbers and signed integers, or fractions, etc.
There are times when we want to see these things, and there are times
when we would like them to be hidden. 
Could one have a "pedantry" knob when editing or browsing agda? 
At pedantry level 11 absolutely nothing would be hidden....

Sergie's gave some examples of using "+", "*" etc to mean different
operations in different rings.  Is this an example of coercion?
I'm inclined to call it overloading.  (Which also helps to dispense with 
pedantic crap.)