Algebraic structures with stable or decidable equality

[Taneb]

In light of #1767, it might be useful to have copies of the algebraic hierarchy with stable equality, and with decidable equality

Here's a very rough sketch of what this could look like

record IsStableMagma {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma _≈_ ∙
    isStable : ∀ x y → Stable (x ≈ y)

record IsDecidableMagma {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma _≈_ ∙
    isDecidable : ∀ x y → Dec (x ≈ y)

  isStableMagma : IsStableMagma _≈_ ∙
  isStableMagma = record
    { isMagma = isMagma
    ; isStable = λ x y → decidable-stable (isDecidable x y)
    }

I've heard that many classical theorems, when you try to prove them constructively, depend on decidablility of equality.

I'm not sure how this interacts with the recently added Apartness things. I suspect that Apartness is weaker than Stable.

[MatthewDaggitt]

If we did add these, then I think we should have different subfolders for them to mirror the Apartness approach. For example, Algebra.Decidable and Algebra.Stable.

[Taneb]

I've been thinking about this recently, and I think there's a hierarchy that goes something like Stable -> Decidable -> Enumerable (not actually sure how to define this)-> Finite (plus maybe Subfinite but I don't know where that goes). (c.f. #1881, I hadn't realised how they interacted when I opened it).

Given that this is getting to be quite a few duplicates of the algebra hierarchy, which is itself already very big, we should maybe consider doing something cleverer. @JacquesCarette I'd be interested in your thoughts here

[JacquesCarette]

Sorry the summoning took so long to actually work, life interfered a lot.

I've definitely thought long and hard about just this problem, and have done some prototype implementations. In theory, this is some kind of "mixin" situation.

Unfortunately, it's a mixin "at the wrong level", i.e. at a part of Agda that is very far from first-class: record declarations. The duplication occurs not at the value level, but at the level of extending the environment with new definitions derived from old ones.

In an internalized representation (think of doing Universal Algebra in Agda), this is all relatively straightforward. The problem is that this results in something highly unusable - the levels of 'coding' is unbearable.

It's tempting to attack this with metaprogramming (external to Agda, as the reflection capabilities aren't up to the job - yet?) but even as an expert on the topic, I think of that "solution" as a patch rather than a long-term solution. A better solution would internalize "parametrized theory presentations" and have a solid elaborator that would let users see where the theory they're working with came from.

Right now, Agda has no tools to let you programmatically build theory networks. [There's even problem building them by hand.]

Having said all of that, I think that exploring the design space via some kind of DSL that generates Agda would make sense. That's essentially what hierarchy-builder does for Coq's mathcomp (via ELPI). (I just wish they'd looked at a dozen or my papers, not just the one!)