Conversation
| to the point halfway along `loop`{.Agda}. However, the only two points | ||
| along the interval that we can name are `i0`{.Agda} and `i1`{.Agda}. | ||
| Thus, we need to map `north`{.Agda} to either `base`{.Agda}, `loop i0`, | ||
| or `loop i1`, since these are the only terms of type `S¹`{.Agda} that we |
There was a problem hiding this comment.
since these are the only terms of type S^1 that we can name
Not technically true, cause we have closed hcomp terms in S^1 that don't reduce (IIUC). Not sure how rigorous this should be though
There was a problem hiding this comment.
Good enough for intuition, but note that loop i0 and loop i1 are base, so there's really only one normal term (ignoring empty hcomps).
There was a problem hiding this comment.
It does say that those are all definitionally base, but yeah I wasn't sure how much people think about irreducible hcomps when thinking about members of HITs
There was a problem hiding this comment.
You could add a footnote mentioning it
|
This seems redundant with our existing proof that the suspension of 2 points is equivalent to S¹? |
|
Hum, the maths is redundant, but the explanation are better. Can we replace that for this? |
Co-authored-by: Naïm Favier <[email protected]>
Oh yeah, of course that proof would have to have a similar approach. Yeah, this shouldn't be a new module then since this HIT is obviously equivalent to
Yes, do you want me to transport (heh) these explanations to that proof in |
5 participants
Description
A new module for an HIT which is essentially S^1 but with two point constructors, along with a proof of equivalence with S^1 and an example of stealing theorems from S^1 given this equivalence. Funnily enough, while cleaning it up, I realized it was actually much simpler than what I shared in Discord, and the only lemmas it needed about composition ended up already existing in other modules.
Checklist
Before submitting a merge request, please check the items below:
support/sort-imports.hs.