<div dir="ltr"><div>Apologies, I didn't send this to the list when I replied the first time round.</div><div dir="ltr"><br></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">Hi Sergei,<br></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> </blockquote><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"></blockquote><div dir="ltr"><span class="gmail-im" style="color:rgb(80,0,80)"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">There are many paths in it which lead to the same Setoid.</blockquote></span></div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> </blockquote><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">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. <br>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...<br>Best,<br>Matthew<br><img class="gmail-ajT" src="https://ssl.gstatic.com/ui/v1/icons/mail/images/cleardot.gif" style="background: url("https://www.gstatic.com/images/icons/material/system/1x/more_horiz_black_20dp.png") 50% 50% / 20px no-repeat; height: 11px; opacity: 0.54; width: 24px;"></blockquote><div dir="ltr"><span class="gmail-im" style="color:rgb(80,0,80)"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br></blockquote></span></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Jun 8, 2020 at 10:42 PM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2020-06-08 14:27, <a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a> wrote:<br>
> There is a tree made by import steps, with the root in Semiring.<br>
> There are many paths in it which lead to the same Setoid.<br>
> Probably the type checker evaluates all these paths to the same tree node<br>
> presenting this setoid.<br>
> Because in a Semiring, +-magma and *-magma share the setoid.<br>
> ?<br>
<br>
I have not checked the example very carefully, but I don't think that<br>
the two setoids are necessarily equal: they might have distinct proofs<br>
of (say) transitivity. Perhaps it would make sense to change the library<br>
so that the two setoids are equal (or to stop using setoids).<br>
<br>
-- <br>
/NAD<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>