Drop equivalence relation from `Algebra.Bundles.Raw` structures?

[carlostome]

Structures currently defined in Algebra.Bundles.Raw (RawMagma, RawMonoid,...) include as part of their definitions the "underlying equality" relation. For example,

record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier

The rationale behind Raw structures (cf. README.Design.Hierarchies) seems to be that they ought to only bundle algebraic operations (e.g. _∙_ : Op₂ Carrier above) in a spirit similar to Haskell's typeclasses.

Wouldn't it make sense to drop the _≈_ relation from these structures?

As a point of comparison, the Raw structure for functor does not include such relation (Effect.Functor):

record RawFunctor (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
  infixl 4 _<$>_ _<$_
  infixl 1 _<&>_
  field
    _<$>_ : (A → B) → F A → F B
  ...

[Taneb]

We're using the _≈_ in the raw algebraic structures to define the laws of homomorphisms. We can't easily remove it.

[carlostome]

Why are these part of the structures as opposed to being parameters of homomorphism?

[jamesmckinna]

Thanks @carlostome for the (challenging!) questions. I hope the rambling discussion below helps...

I'd make two observations before going away to try to think a bit harder about this (and probably nudge @JacquesCarette and @MatthewDaggitt for comment...):

• I think the comparison with (Raw)Functor is problematic, or at least, not immediately applicable, precisely because the design there has always foundered on the difficulty of how to capture, in general, the 'right' notion of equality on arbitrary F A in order to be able to correctly formulate the laws...; by contrast, within a given algebraic structure, the 'parameter' wrt which the algebraic laws are formulated, namely _≈_ is readily captured; but for all that, it is still a design choice as to whether you include equality as part of the 'raw' signature or not, and @Taneb makes one argument for it (all design choices eventually come down to such pragmatics in the end?)
• regarding parameterisation, for sure we could have completely unbundled parameter telescopes everywhere (a meta-design principle of minimum commitment), and indeed we still see vestiges of this in the long telescopes associated with the Algebra.Structures.IsX structures... so much so that I have argued against the current design, in favour of making (a version of) the Raw bundles as a single parameter to the IsX structures in #2252 , and there, I don't think it would make sense to omit the relation, precisely because the specification of laws requires the relation... (my only point of divergence would be to make the underlying {A : Set a} be a parameter to Raw bundles, rather than an explicit field... there's a separate discussion to be had there about 'sharing by parametrisation'/'Pebble-style' sharing which, though relevant here, is a bit too wide a scope for your questions, I think?)

For better or worse (and certainly, pre the development of HoTT/cubical ideas around making equality a global/ambient property of types), stdlib makes the choice ('Bishop-style'?) of a (pre-)Setoid-based organisation of the library design of all/most of the basic abstract objects in the library. Changing that now would be... a major undertaking, and a significant fork in the design space.

The (not an exact one, though!) analogy from universal algebra (I think! UA experts please correct me if not) is whether or not equality is taken as explicit part of the relational signature, or presupposed. Making equality part of the Raw bundle is (a version of) the 'presupposed' design choice.

The 'dirty' reason underlying such a choice is precisely (?) to avoid marshalling and unmarshalling an explicit (Raw)Setoid object underlying any given algebraic structure (or correspondingly at any higher level of abstraction), with all the space+time complexity disadvantages that would entail. In an ideal implementation, such marshalling/unmarshalling would be cost-free (@JacquesCarette has looked at this extensively with his students, and it's implemented, IIUC, in the Arend system) but that is not, alas, where we are with Agda.

Lastly, I'm always reluctant to take too seriously any comparison with haskell typeclasses, precisely because, by not having to take laws seriously, they avoid all the hard work in figuring out a workable design for 'real' algebraic structure (never mind the compromises entailed by having type-checking based on (unique) instance inference...)

[jamesmckinna]

Under propositions-as-types, I'd be tempted to go out on a limb and say that the 'operational signature' ('syntax') of an algebra includes/should include the 'relational signature', since together they define the language in which the equations ('semantics') can be stated as properties expressed relative to such a vocabulary... but that's probably a reach too far, philosophically at least?

After all, the ordered structures under Relation.Binary take their equality and ordering symbols as parameters to the IsX structures... although as we don't yet have Raw versions of the corresponding bundles #2491 its not a fair comparison ...

TL;DR: I think the orthodox first-order model theory distinction between function symbols and relations is artificial, just as is that between 'expressions' and 'terms' as to well-formedness wrt a possibly non-context-free grammar.

[jamesmckinna]

And... finally: what would we do if we went beyond purely first-order algebraic signatures to essentially algebraic, where equality plays a role in even defining well-formedness of terms (eg specifying pullbacks as a 'function' of conical data)?