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.

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

Rename (co)prod to (co)product #1017

Merged
merged 9 commits into from
Feb 6, 2024
Merged

Conversation

fredrik-bakke
Copy link
Collaborator

No description provided.

@EgbertRijke
Copy link
Collaborator

I added a new label "improve naming" because this PR is a quick global search-and-replace that improves our naming. I thought such a label would be more descriptive than "refactoring", because refactoring suggests that you actually factor out steps or clean up to make the code simpler. I'd be happy to put the label back if you think it is more fitting.

BTW I am a bit afraid of quick search-and-replace changes since they are (1) so quick to make but (2) easily jinx other people's work. But I think this one is not actually causing so much trouble.

@fredrik-bakke
Copy link
Collaborator Author

There was one naming conflict that came up when making this refactoring. Namely, prod-Precategory referred to the product of two precategories, while product-Precategory referred to the product of two objects in a precategory. I consider this bad practice, and propose that we refer to the latter as product-obj-Precategory instead, suggesting a general scheme such as, for instance, pullback-hom-Precategory for a pullback of a morphism in a precategory. I thus renamed

  • pullback-Precategory to pullback-obj-Precategory,
  • coproduct-Precategory to coproduct-obj-Precategory,
  • exponential-Precategory to exponential-obj-Precategory.

I consider this PR ready for review again. I can take a quick look over it first during my layover if you prefer, as this is a quick search-and-replace job as you suggested.

@fredrik-bakke
Copy link
Collaborator Author

(This also suggests that we may want to change our naming scheme for category theory modules as well. Something I suggest we have a look at when we start doing wild category theory soon.)

@EgbertRijke
Copy link
Collaborator

There was one naming conflict that came up when making this refactoring. Namely, prod-Precategory referred to the product of two precategories, while product-Precategory referred to the product of two objects in a precategory. I consider this bad practice, and propose that we refer to the latter as product-obj-Precategory instead, suggesting a general scheme such as, for instance, pullback-hom-Precategory for a pullback of a morphism in a precategory. I thus renamed

  • pullback-Precategory to pullback-obj-Precategory,
  • coproduct-Precategory to coproduct-obj-Precategory,
  • exponential-Precategory to exponential-obj-Precategory.

I consider this PR ready for review again. I can take a quick look over it first during my layover if you prefer, as this is a quick search-and-replace job as you suggested.

Are you sure that it won't be confusing if pullback-hom-Precategory should mean a pullback, and not a pullback-hom?

@fredrik-bakke
Copy link
Collaborator Author

Good point!

@fredrik-bakke
Copy link
Collaborator Author

We will have to disambiguate that special case somehow. Otherwise, do you disagree it is a solid scheme?

@EgbertRijke
Copy link
Collaborator

EgbertRijke commented Feb 5, 2024

If it's ok with you I will wait with merging this PR until #1014 is merged, because I don't look forward to hours of resolving merge conflicts whereas a much quicker solution would be that you just do your search-and-replace again if there are any problems.

@fredrik-bakke
Copy link
Collaborator Author

If it's ok with you I will wait with merging this PR until #1014 is merged, because I don't look forward to hours of resolving merge conflicts whereas a much quicker solution would be that you just do your search-and-replace again if there are any problems.

Sure thing!

@EgbertRijke
Copy link
Collaborator

We will have to disambiguate that special case somehow. Otherwise, do you disagree it is a solid scheme?

The scheme with pullback-obj-Precategory has no obvious problems, so I agree.

Copy link
Collaborator Author

@fredrik-bakke fredrik-bakke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I had a look at about 50 of the files. Looks good to merge to me

@EgbertRijke EgbertRijke merged commit 1fb68af into UniMath:master Feb 6, 2024
4 checks passed
@fredrik-bakke fredrik-bakke deleted the prod branch February 6, 2024 20:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants