[Agda] Re: Accessing fields of algebra records

[Sergei Meshveliani]

N. Raghavendra responds

> At 2015-03-10T16:36:05+04:00, Sergei Meshveliani wrote:

        >> This leads to a very large expression. And this is replaced with  
        >>
        >> open Semigroup Ring.+semigroup R using () renaming (_∙_ to _+_)

> If we replace Semigroup with IsCommutativeMonoid, Ring.+semigroup with
> CommutativeSemiring.*-isCommutativeMonoid, and R with
> NatProp.commutativeSemiring, and omit the using/renaming parts, in your
> example above, it looks quite like what I'd written, namely,
>
> 1*n≡n : (n : ℕ) → 1 * n ≡ n
> 1*n≡n = identityˡ
>  where
>    open IsCommutativeMonoid
>      (CommutativeSemiring.*-isCommutativeMonoid NatProp.commutativeSemiring)
>
> I was only wondering if there's an easier way to call the various
> forgetful functors.


It could be simpler:

            CommutativeSemiring.identityˡ NatProp.commutativeSemiring

But probably, CommutativeSemiring  of  stdlib  contains both `identity' 
for _*_ and for _+_
(I use a bit another hierarchy, and it is difficult for me to inspect this 
feature in stdlib). 

Probably, this is why you are forced to mention one more level:
*-isCommutativeMonoid.

If `identity' was not ambiguous in this sense, it would be resolved due to 
setting  "open _ public"  in certain places in the nested records
(probably stdlib uses  "open _ public"  this way).

Do I mistake?

Regards,

------
Sergei