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

Replace ab_biprod_corec_eta with grp_prod_corec_natural #2085

Merged
merged 1 commit into from
Sep 12, 2024

Conversation

jdchristensen
Copy link
Collaborator

Since we generalized ab_biprod_corec to grp_prod_corec, we should also generalize ab_biprod_corec_eta to grp_prod. In the process, I renamed it from _eta to _natural. It's a definitional equality that isn't used anywhere, but is probably worth keeping as a form of documentation.

I had to switch grp_prod_corec to use wildcat notation, and I switched a couple of nearby things as well.

@Alizter
Copy link
Collaborator

Alizter commented Sep 12, 2024

Switching GroupHomomorphism to $-> will introduce a strictly larger universe in those expressions, but as we've said before we don't care when algebraic universes land. (Which by the way are still being worked on, just optimizing the new algorithm is a bit slow).

@jdchristensen jdchristensen merged commit 43b2ccd into HoTT:master Sep 12, 2024
22 checks passed
@jdchristensen jdchristensen deleted the grp_prod_corec branch September 12, 2024 13:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants