2.1 Definitions that might be unnecessary and possibly omitted

[williamdemeo]

(2.1 references item 1 of referee report 2)

Some definitions and proofs look unnecessary and therefore lack motivation. In particular,

• The referee says we could parameterize FreeAlgebra by a class of algebras K rather than by a relation E on terms, and defines the FreeDomain F[X] as the quotient of Term X by Th K; then the inductive relation ⊢▹≈ (and related proofs, soundness) are unnecessary for the proof of Birkhoff to carry on.

  (The original proof did what the referee suggests, but we switched to the approach that requires Abel's ⊢▹≈ relation because (I think) with the former approach we ran into trouble completing the proof and actually introduced an inconsistency.)

• Second half of the paper (starting with § on relatively free algebra) is confusing. The referee suggests the following argument:

  Define F[X] as T X / ~, where x ~ y iff given any homomorphism f into an element of K, f x = f y (in other words, x ~ y iff (x,y) ∈ Th K). Then, if A is in Mod (Th K), the surjective morphism T A → A factors through T X → F[X], so it remains to show that F[X] ∈ SP K (then, A ∈ HSP K).

  F[X] is easily shown to be a sd prod of all algebras in K. However, because of size issues, this product may not exist. Fortunately, it's also a subproduct of the algebras in {T X / Θ}, because any hom factors as an epimorphism followed by a monomorphism, so that x ~ y iff for any epimorphism f into an element of S K, f x = f y.

  This argument is close to ours, but might be more understandable (provided it's correct).

[JacquesCarette]

Do we have the time to deal with this in the time remaining? Seems big! I'd want to leave this to last.

[williamdemeo]

I dispensed with this by explaining (in the response to referees) that we tried this approach but couldn't get it to work without introducing an inconsistency and that, by borrowing from Abel's elegant approach to contexts and environments, we were able to avoid the inconsistency.

We should probably point this out in the paper as well, so readers don't also wonder whether we tried to formalize the approach suggested above.

I'll do that now.

[JacquesCarette]

Should be careful to not say that the method can't work, just that we couldn't make it work. Understanding the 'why' could be pointed out at potential future work.

[williamdemeo]

Good point. 👍

On Thu, Apr 28, 2022 at 12:02 PM Jacques Carette @.***> wrote:

Should be careful to not say that the method can't work, just that we couldn't make it work. Understanding the 'why' could be pointed out at potential future work.

— Reply to this email directly, view it on GitHub https://github.com/ualib/agda-algebras/issues/191#issuecomment-1112385223, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA25MJG5MUORQPNLBSACCOLVHKY7PANCNFSM5UG2PQYA . You are receiving this because you authored the thread.Message ID: @.***>