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

[James Wood]

Yes. You can tell how many there are by writing out an inhabitant and
noticing how many times you have to prove an `IsEquivalence`.
`CommutativeRing` will have two because these ultimately come from the
two magmas (addition and multiplication).

Best wishes,
James

On 08/06/2020 19:50, mechvel at scico.botik.ru wrote:
> 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
>>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>