Get rid of inconsistent `∙-cong` name in algebra hierarchy?

[MatthewDaggitt]

Every other property in the algebraic (not to mention in Relation.Binary etc.) structures are simply named assoc/comm etc. unless the structure contains two operators in which case they are prepended with the operator name(s).

The exception to this rule is the congruence proof which is incongruously named ∙-cong. https://github.com/agda/agda-stdlib/blob/b09525ccb0b0d0993ecbd3123eae1e72046b8263/src/Algebra/Structures.agda#L36

We should have a discussion about whether we should rename this to simply cong in version 2.0.

As I see it:

Pros

• More consistent
• Easier to type (frequently get confused about whether it's \. \cdot or \bub in certain fonts)

Cons

• May clash with cong from Relation.Binary.PropositionalEquality a lot.

[JacquesCarette]

That con could be a really big one. So I headed over to Algebra.Properties to find out how bad it would be... and it would be fine. They are not used together there!

So I started writing this comment being quite against it (because of the con), and when I went digging for data... didn't find it. This could be worse in code bases "out there", I don't know. But internally to the library itself, this doesn't look like a big deal.

[MatthewDaggitt]

So I started writing this comment being quite against it (because of the con), and when I went digging for data... didn't find it. This could be worse in code bases "out there", I don't know. But internally to the library itself, this doesn't look like a big deal.

Anecdotally, I also rarely use them together. As I'm very keen on having small modules that do one thing, either I'm working with setoid based equality from some algebraic structure or I'm working with propositional equality. However, it may have a greater impact on people who tend to throw everything together in bigger files...

[jamesmckinna]

Middle ground: why not cong₂? Won't you also need a unary version (cong₁?) as well? And yes, I know the contra above would still be a potential problem, but much less common than that arising for cong itself (it's a pity about the pre-existing cong₂)?

[jamesmckinna]

What happens in your proposed scheme to the properties ∙-congˡ and ∙-congʳ?

[MatthewDaggitt]

They would become congˡ and congʳ

[jamesmckinna]

v2.0?

[jamesmckinna]

For whatever reason (but see numbers below), I'm going to press on my proposal to rename to cong₂ (and cong₁ where appropriate, along with @MatthewDaggitt 's left-/right- names). The definitions in Algebra.Definitions have no compunction about the subscripting, and relative to PropositionalEquality, we (appear to) have

• 100+ uses of ∙-cong, relative to 250 uses of cong₂, compared to 2500+ uses of cong

[figures approximate, based on rubbish grepping; and these are merely occurrences, rather than attempting to track actual/potential clashes, but clearly the potential clash rate is already reduced by an order of magnitude by the proposal... ;-)]

[jamesmckinna]

Opening a related issue for v2.0-rc1...

[jamesmckinna]

Revisiting this, I am (now) conscious that the opposite choice is already made regarding the name of the homomorphism property in Algebra.Morphism.Structures.IsMagmaHomomorphism, which for whatever reason, is called homo, whereas all the subsequent field names for such properties are tagged by the associated piece of syntax, viz. ε-homo for IsMonoidHomomorphism, etc.

Correspondingly, congruence for ⁻¹_ is ⁻¹-cong in the definition of Algebra.Structures.IsGroup... etc.

So I'm tempted to conclude that we should, in fact, retain the name ∙-cong, and moreover rename Algebra.Morphism.Structures.IsMagmaHomomorphism.homo to ∙-homo...?

This seems to arise from the v1.5 deprecations in Algebra.Morphism, some of whose definitions (moreover of syntax!) nevertheless still appear in eg Data.Nat.Properties (thanks to suppression of the deprecation warnings... sigh)

UPDATED: seemingly only 15 uses of such homo in the library needing to be updated?

[jamesmckinna]

Should we close this now, in favour of #2458 / #2464 ? Or is this issue sufficiently 'orthogonal' to be left open?

[JacquesCarette]

I do believe we should close this one, since it is about going in the 'wrong' direction.