Equivalence between the first sphere and the circle

[maybemabeline]

I'm sorry for not consulting with anyone before jumping into this project but to be honest I thought it was going to be a lot simpler. It turned out that last year's HoTTest summer school where I had already seen and formalized this statement postulated some more judgmental equalities than the unimath library does, so this ended up a lot longer. If anyone was planning on doing a more systematic treatment of the spheres, I have no problem with this not being merged. Otherwise, here it is.
I opted to just use concatenation instead of equational reasoning because I felt like writing out all the intermediate terms wouldn't really add any clarity to the path algebra and only clutter things.
I ended up adding another function for computing dependent identifications over eq-value, as I think it could have some general usefulness for proving maps are inverses.

[EgbertRijke]

Beautiful! Your code was already very close to our conventions, that's why I was able to give so much detail.

Well done!

[maybemabeline]

Thank you for the corrections! I'm afraid one of them seems to have broken something though. Is there any way to tell which one?

[EgbertRijke]

Thank you for the corrections! I'm afraid one of them seems to have broken something though. Is there any way to tell which one?

I'm sorry for this! I might have misinterpreted one of your long identifications. It was possibly another inverted path again, where I didn't see the scope of inv correctly. If you type-check it, it should tell you which term doesn't go through.

If you have trouble correcting the code, let me know again, because I can also pull your branch and see if I can solve it.

[EgbertRijke]

I found the problem:

On line 170,

  up-suspension-meridian-suspension
    ( sphere 0)
    ( 𝕊¹)
    ( suspension-structure-sphere-0-𝕊¹ (zero-Fin 1))

should be replaced with

  up-suspension-meridian-suspension
    ( sphere 0)
    ( 𝕊¹)
    ( suspension-structure-sphere-0-𝕊¹)
    ( zero-Fin 1)

[EgbertRijke]

Note that the merged suggestions of this PR might have altered the code on your branch, so you need to do git pull to get the changes locally. And then line 170 should have up-suspension-meridian-suspension on it.

[maybemabeline]

I already found it too :)

[EgbertRijke]

Actually, I feel like you can just add this equivalence to synthetic-homotopy-theory.circle. We usually don't have separate files for constructions of equivalences. It is true that this one is quite elaborate, but on the other hand it is also clearly a property of the circle, so it would naturally go into that file. Would you be willing to do that?

It would go at the end of the file under ## Properties and you can make a section ### The circle is equivalent to the 1-sphere. The text that you currently have in your ## Idea section can also go under here.

[maybemabeline]

Actually, I feel like you can just add this equivalence to synthetic-homotopy-theory.circle

Alright! At first I wrote this in the spheres module but that didn't feel quite right. Moving it to the circle module sounds like a good idea.

[EgbertRijke]

Actually, I feel like you can just add this equivalence to synthetic-homotopy-theory.circle

Alright! At first I wrote this in the spheres module but that didn't feel quite right. Moving it to the circle module sounds like a good idea.

Yep, I think your intuition was right! The file about general spheres should be for properties about general spheres, and not for properties specialized about the 1-sphere or the 2-sphere or any other specific n-sphere.

[maybemabeline]

I changed around the order of some things so that the construction would be more about the circle, now that it's in the circle module.
I hope the accompanying explanation didn't end up too verbose. Feel free to correct something again if you think the language isn't precise enough.

[VojtechStep]

I'm not sure how discoverable the link-check CI is for new contributors: if you click on "Details" on the action, it will tell you which link targets it didn't find; currently you're referencing synthetic-homotopy-theory.suspensions.md and foundation-core.identifications.md, which don't exist (the correct targets are synthetic-homotopy-theory.suspensions-of-types.md and foundation-core.identity-types.md, respectively).

[EgbertRijke]

My bad! I suggested those links that don't exist without checking.