search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
219 stars 70 forks source link

Eckmann-Hilton Updates #1133

Closed morphismz closed 2 months ago

morphismz commented 5 months ago

Fixes links and makes consistent naming changes related to the Eckmann-Hilton file. Also adds an updated reference to the page.

fredrik-bakke commented 5 months ago

Hey Raymond, welcome back! It's good to see you're active again. Looking forward to seeing what's coming next. 🙂

morphismz commented 5 months ago

Hey Raymond, welcome back! It's good to see you're active again. Looking forward to seeing what's coming next. 🙂

Hey Fredrik, thanks! I'm spinning up for the summer, hoping to get a good chunk of math formalized. Hoping to get the Hopf fibration finally all formalized. I figured I'd acquaint myself with the updates to the library by making a few small prs first. Though it seems like I should reacquaint myself with the style guide first :smile:

morphismz commented 4 months ago

I've added a bit more work to this pr. The main result is a finished computation of transporting along an eckmann-hilton identification, resolving one of the tasks in issue #702 .

There is a bit more clean up I need to do before this pr is ready for review. I'll mark it ready when the time comes.

morphismz commented 4 months ago

I think this pr is now ready for review. There is one more lemma I will add later, namely computing transport along the eckmann-hilton 3-loop. But this relies on some infrastructure related to 3-automorphisms that I will be building in a different pr. So that lemma will wait.

Please let me know if I should tone down the prose, I feel like there is a lot on the Eckamnn-Hilton page. I added a bit of an explanation of how we compute transport along an Eckmann-Hilton identification. Let me know if there should be more or less of an explanation

morphismz commented 4 months ago

Those coherences look like a major PITA

Yes, yes they were...

Thanks for the diligent review process and all the feed back!

morphismz commented 2 months ago

Okay, I tried messing around with the diagrams a bunch, but I couldn't get anything to look nice. I'll delete them for now, so this pr can get merged. I'll keep thinking about ways to explain those coherence (maybe linking to some external diagrams, idk). If I come up with something, I'll add that in another pr.

But, for now, I figured, I'll just try to get this pr merged.

morphismz commented 2 months ago

brother, you'd think I'd know how to spell concatenation by now

morphismz commented 2 months ago

Thanks for all the help on this pr @VojtechStep , and sorry again for the quite drawn out process

VojtechStep commented 2 months ago

My pleasure, and no worries, my schedule was also pretty tight, so I'd say the drawing-out was mutual 😅