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

shorter proofs of monoidal structure in Products.v #1943

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented May 2, 2024

By not going through the twist construction for the pentagon and hexagon in Products.v we can make the proof shorter. This is because we can efficiently compute the projections of an associator.

This was needed in #1929 so that we could more easily work with the associator.

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 71fedf78-ccf4-43b4-a08b-0441d4f782b6 -->
@Alizter Alizter requested a review from jdchristensen May 2, 2024 19:58
@jdchristensen
Copy link
Collaborator

It's hard to tell whether the smaller proofs of the hexagon and pentagon are mainly due to not using the twist or due to the various helper lemmas you added. It's definitely smart to add and use those lemmas! And since that path algebra is so tricky, I don't think it's worth investigating whether the twist approach could be equally short. So, this LGTM.

(BTW, it just occurred to me that the lhs and rhs tactics could probably be adapted to work for any transitive relation, so they could be used for $==, ==, <~>, etc. That would probably help with these proofs!)

@Alizter
Copy link
Collaborator Author

Alizter commented May 2, 2024

It's hard to tell whether the smaller proofs of the hexagon and pentagon are mainly due to not using the twist or due to the various helper lemmas you added. It's definitely smart to add and use those lemmas! And since that path algebra is so tricky, I don't think it's worth investigating whether the twist approach could be equally short. So, this LGTM.

For the pentagon, its a matter of size. Reducing 5 terms is inherently shorter than reducing 9 terms. I know this because I originally shortened the pentagon proof to use some similar lemmas and then avoided the twist construction.

For the hexagon, I didn't try the twist construction directly. But presumably because the proof fits on my monitor it is good enough.

Again, this is only because products have this nice property that we can prove these lemmas more easily. So this idea doesn't apply to other monoidal products like the join. Although, for the join it's not entirely certain yet if the 9-gon axiom is manageable yet.

(BTW, it just occurred to me that the lhs and rhs tactics could probably be adapted to work for any transitive relation, so they could be used for $==, ==, <~>, etc. That would probably help with these proofs!)

Yes, I also had this thought a few times to. I would definitely welcome such a PR.

@Alizter Alizter merged commit 1c4071d into HoTT:master May 2, 2024
23 checks passed
@Alizter Alizter deleted the ps/rr/shorter_proofs_of_monoidal_structure_in_products_v branch May 2, 2024 21:21
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.

None yet

2 participants