Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Get rid of inconsistent homo name in algebra hierarchy? #2458

Open
jamesmckinna opened this issue Aug 15, 2024 · 5 comments · May be fixed by #2464
Open

Get rid of inconsistent homo name in algebra hierarchy? #2458

jamesmckinna opened this issue Aug 15, 2024 · 5 comments · May be fixed by #2464
Labels
breaking discussion naming

Comments

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Aug 15, 2024 •
edited
Loading

Revisiting #1544, 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?

Originally posted by @jamesmckinna in #1544 (comment)

This is the 'complementary'/'counter' issue to #1544 , again in pursuit of consistency/uniformity, but in the 'opposite' direction to that issue. In such a narrow sense, we should agree to solve only one of these, and not the other, but in the interests of a 'balanced' discussion, worth separating out, I think!?

UPDATED: looking at #2464 it seems that there are in fact 21 bindings of the field name, and a further 23 uses of it... assuming that I have caught them all!
@JacquesCarette
Copy link
Contributor

The data, at the time, didn't support my 'hunch' that ∙-cong was the better way to go.

Really, cong for an n-ary operator should take that operator symbol as input, rather than as a baked-in name. But I don't think Agda is ready for that, so ∙-cong is the current best that can be done?

@jamesmckinna
Copy link
Contributor Author

While I agree with the general principle that cong (and homo!) should key off the (arity of the) symbol being characterised... if we attempted that we'd get so much ambiguity in the field names as the record hierarchy builds up that I just don't think Agda could cope...

... so the conclusion I drew as regards ∙-cong was, as here, to stick with status quo (contra @MatthewDaggitt ) for that name, and hence for consistency's sake to emulate that here for homo...

@JacquesCarette
Copy link
Contributor

Right - I did want to abstractly discuss hypothetical-rewrite, and agree that the current best solution is to embed the name of the operation in the name, consistently.

@MatthewDaggitt
Copy link
Contributor

Okay, happy to go with embedding the name as part of the operator as standard!

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Aug 29, 2024
@jamesmckinna
fixes agda#2458
9d310ab
@jamesmckinna jamesmckinna linked a pull request Aug 29, 2024 that will close this issue
Open
@jamesmckinna
Copy link
Contributor Author

@JacquesCarette comments as to whether this would be a breaking change? On that basis, so too should this issue be!

@jamesmckinna jamesmckinna mentioned this issue Aug 31, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
breaking discussion naming
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Rename homo to ∙-homo in Algebra.Morphism.Structures jamesmckinna/agda-stdlib
3 participants
@JacquesCarette @MatthewDaggitt @jamesmckinna