[Agda] problem with algebraic hierarchy

[a.j.rouvoet]

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. 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.

Cheers,

Arjen

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