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

Syllepsis #590

Merged
merged 110 commits into from
Aug 23, 2021
Merged

Syllepsis #590

merged 110 commits into from
Aug 23, 2021

Conversation

aljungstrom
Copy link
Contributor

This PR contains a proof of the syllepsis (Eckmann-Hilton p q ≡ (Eckmann-Hilton q p) ⁻¹) for 3-loops p and q. I think the proof can be shortened a bit by using EH-alt as the main definition of Eckmann-Hilton (to avoid transports). I'll make this PR a draft for now and get back to it later.

@ecavallo I remember you had another proof of Eckmann-Hilton. It's possible that the same idea applied to your proof would make things shorter. Do you still have it somewhere? I seem to have lost the link.

@aljungstrom aljungstrom marked this pull request as draft August 12, 2021 00:58
@aljungstrom aljungstrom marked this pull request as ready for review August 13, 2021 09:03
@aljungstrom
Copy link
Contributor Author

@mortberg It doesn't get much shorter than this (for me at least). I think it can be merged.

@mortberg mortberg merged commit 3470593 into agda:master Aug 23, 2021
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.

4 participants