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.

Sign up for GitHub

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
+164 −0
Open

defn: two point circle #324

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d00edf8
defn: two point circle
KevOrr Dec 19, 2023
8c5bcbc
Update src/Homotopy/Space/Circle/TwoPoint.lagda.md
KevOrr Dec 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Update src/Homotopy/Space/Circle/TwoPoint.lagda.md 
Co-authored-by: Naïm Favier <[email protected]>
@KevOrr @ncfavier
KevOrr and ncfavier authored Dec 19, 2023
commit 8c5bcbcb09172022b6d5c67d8373cf1d1692a39c
2 changes: 1 addition & 1 deletion src/Homotopy/Space/Circle/TwoPoint.lagda.md
View file
Original file line number Diff line number Diff line change
@@ -80,7 +80,7 @@ can name. However, all three of these terms are definitionally
S¹₂→S¹ north = base
```

The question now arrises how we map `east`{.Agda} and `west`{.Agda} onto
The question now arises how we map `east`{.Agda} and `west`{.Agda} onto
`S¹`{.Agda}. Recall that the composition `east ∙ west` should map to
`loop`{.Agda}. If we map `east`{.Agda} to `refl`{.Agda}, and
`west`{.Agda} to `loop`{.Agda}, then there will indeed be a path from