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

[Matthew Daggitt]

Apologies, I didn't send this to the list when I replied the first time
round.

Hi Sergei,
>


There are many paths in it which lead to the same Setoid.
>
>

Unfortunately this is not true. The `Setoid`s from `+-magma` and `*-magma`
> in your examples are different setoids. They have the same binary equality
> relation, but the proof of `isEquivalence` may differ and therefore Agda
> does not consider them identical.
> This is not a problem with Agda, but with how the record hierarchy is
> designed. I'm not sure there is a good solution for the problem, short of
> parameterising every record in the hierarchy by a `Setoid`. However that
> brings its own set of problems...
> Best,
> Matthew
>

>
On Mon, Jun 8, 2020 at 10:42 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200608/1778956d/attachment.html>