[Agda] problem with algebraic hierarchy

[mechvel at scico.botik.ru]

On 2020-08-10 19:27, a.j.rouvoet wrote:
> Dear Sergei,
> 
> The problem you encounter is wellknown under the name 'the
> (un)bundling problem':
> i.e., the problem of choosing which fields should be parameters, and
> which should be fields.
> The problem is hard, in the sense that every permutation you can think
> of has applications.
> The Agda standard library chooses to do what most other languages have
> done previously: i.e., provide a unbundled IsStructure, and a bundled
> Structure.
> 
> The variation you propose has merits, but equally many demerits.


I have provided two sensible examples showing a merit.
Can you provide a sensible example showing a demerit?

A generic discourse, notes, objections can be understood when there are 
given examples.
Very often I start to understand of what I intend to tell only after 
considering examples.
I expect the same is, more or less, with other authors.

Regards,

--
SM



> Until we can dynamically bundle/unbundle, I don't think there is much 
> to be
> said for a particular different variation.
> There has been some recent attention for this language feature by
> various people and the Arend proof assistant.
> [..]



> On 8/10/20 6:04 PM, mechvel at scico.botik.ru wrote:
>> We wrote the following to GitHub for the library:
>> 
>> mechvel
>> -------
>> I wonder: how to express in Agda-2.6.1 + lib-1.3 the following 
>> discourse?
>> Let R and U be semirings having the same additive monoid 
>> (+-commutativeMonoid).
>> Denote * and *' the multiplication operators in R and U respectively,
>> 1# and e the unities in R and U respectively. Prove in Agda that
>> 
>> for all x in R  it holds  (1# + 1#) * x ≈ (e + e) *' x     -- (I)
>> 
>> And let us assume that the lemma 2*as+ : ∀ x → (1# + 1#) * x ≈ x + x
>> is proved in the module OfSemiring parameterized by Semiring
>> (it is proved simply in 2-4 steps).
>> Mathematically, the statement (I) has sense.
>> And its proof is simple: the left hand side equals x + x by the laws 
>> of R;
>> the right hand side equals x + x by the laws of U, and this is the 
>> same
>> element of their common Carrier.
>> The matter is not in the proof itself, it is in finding a valid 
>> formulation
>> of the theorem (I) in Agda.
>> Can anybody, please, demonstrate?
>> 
>> 
>> Matthew Daggitt
>> ---------------
>>> This is not a question for the standard library.
>>> Best to ask this on the mailing list.
>> 
>> 
>> No, it is for the standard library.
>> But let it be, I write to the Agda list.
>> 
>> For example, if the library was organized in a different way, the 
>> following code would work:
>> 
>> -----------------------------------------
>> theorem : ∀ {α α≈} (S : Setoid α α≈) (+cMon : CommutativeMonoid S)
>>                                      (*Mon  : Monoid S)
>>                                      (*'Mon : Monoid S)
>>                    (R : Semiring S +cMon *Mon) (U : Semiring S +cMon 
>> *Mon) →
>>                    let open Semiring R
>>                        open Semiring U using ()
>>                                        renaming (_*_ to _*'_; 1# to e)
>>                    in
>>                    (x : Carrier) → (1# + 1#) * x ≈ (e + e) *' x
>> 
>> theorem S R +cMon *Mon *'Mon R U x =
>>     begin
>>       (1# + 1#) * x  ≈⟨ OfSemiring.2*as+ R x ⟩
>>       x + x          ≈⟨ sym (OfSemiring.2*as+ U x) ⟩
>>       (e + e) *' x
>>     ∎
>> ------------------------------------------
>> 
>> Here Magma, Semigroup, Monoid, CommutativeMonoid  have an argument of 
>> the Setoid type.
>> Semiring has arguments (S : Setoid _ _), (+M : CommutativeMonoid S),
>> (*M : Monoid S).
>> 
>> Also this solves the problem of a common setoid for +-magma and 
>> *-magma in a semiring
>> (of what we wrote earlier).
>> 
>> I do not say that everything is all right there.
>> But generally, it has sense to think of experimental libraries that 
>> reorganize the
>> algebraic part, of different ways to transfer the domain parameters.
>> 
>> The first step may be setting (S : Setoid) as an argument as above.
>> This will improve much, without spoiling anything.
>> But I am not sure that this will be sufficient.
>> 
>> Regards,
>> 
>> ------
>> Sergei
>> _______________________________________________
>> 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