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

defn: two point circle #324

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Conversation

KevOrr
Copy link

@KevOrr KevOrr commented Dec 19, 2023

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:

  • I've read the contributing guidelines.
  • The imports of new modules have been sorted with support/sort-imports.hs.
  • All new code blocks have "agda" as their language.

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
Copy link
Author

@KevOrr KevOrr Dec 19, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Author

@KevOrr KevOrr Dec 19, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@ncfavier
Copy link
Member

This seems redundant with our existing proof that the suspension of 2 points is equivalent to S¹?

@plt-amy
Copy link
Member

plt-amy commented Dec 19, 2023

Hum, the maths is redundant, but the explanation are better. Can we replace that for this?

@Lavenza
Copy link
Member

Lavenza commented Dec 19, 2023

Pull request preview

@KevOrr
Copy link
Author

KevOrr commented Dec 19, 2023

This seems redundant with our existing proof that the suspension of 2 points is equivalent to S¹

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 Sⁿ⁻¹ 2

Can we replace that for this?

Yes, do you want me to transport (heh) these explanations to that proof in Homotopy.Space.Sphere.html?

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