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.

agda-stdlib/src/Algebra/Structures.agda

Line 36 in b09525c

∙-cong : Congruent₂ ∙

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