[Agda] many ways to import the same thing from record

[Nils Anders Danielsson]

On 2020-06-08 14:27, mechvel at scico.botik.ru wrote:
> There is a tree made by import steps, with the root in Semiring.
> There are many paths in it which lead to the same Setoid.
> Probably the type checker evaluates all these paths to the same tree node
> presenting this setoid.
> Because in a Semiring, +-magma and *-magma share the setoid.
> ?

I have not checked the example very carefully, but I don't think that
the two setoids are necessarily equal: they might have distinct proofs
of (say) transitivity. Perhaps it would make sense to change the library
so that the two setoids are equal (or to stop using setoids).

-- 
/NAD