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

pinch map of suspension #1845

Merged
merged 3 commits into from
Feb 12, 2024
Merged

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Feb 12, 2024

We define the pinch map of a suspension and show that it computes accordingly with the wedge projections.

Copy link
Collaborator

@jdchristensen jdchristensen left a comment

Choose a reason for hiding this comment

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

LGTM once the minor changes are done.

theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
@jdchristensen
Copy link
Collaborator

I also noticed the "necessary" is spelled wrong twice in unchanged comments. Maybe you can fix those while you are editing this file?

@Alizter Alizter force-pushed the ps/branch/pinch_map_of_suspension branch from 9f0b77f to 283d936 Compare February 12, 2024 21:00
@Alizter
Copy link
Collaborator Author

Alizter commented Feb 12, 2024

@jdchristensen I've addressed your comments now.

theories/Homotopy/Wedge.v Outdated Show resolved Hide resolved
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter force-pushed the ps/branch/pinch_map_of_suspension branch from 283d936 to 3f26a1a Compare February 12, 2024 21:08
@Alizter Alizter merged commit f08ef4b into HoTT:master Feb 12, 2024
23 checks passed
@Alizter Alizter deleted the ps/branch/pinch_map_of_suspension branch February 12, 2024 21:29
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.

2 participants