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

[mechvel at scico.botik.ru]

Now, what people would tell:
having, say, R : CommutativeRing _ _,
how many different setoids are obtained by various sequences of `open'
applied to the parts of the record (CommutativeRing R) ?
Are there only two of them?
((Magma.setoid +-magma) and (Magma.setoid *-magma))
?

--
SM


On 2020-06-08 17:49, Matthew Daggitt wrote:
> [..]
>> 
>>> 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