defn: two point circle

[KevOrr]

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:

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

[ncfavier]

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

[plt-amy]

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

[Lavenza]

Pull request preview

[KevOrr]

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?