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

Jump to bottom

Refactoring pointed types #1056

Merged
merged 55 commits into from
Mar 13, 2024
Merged

Refactoring pointed types #1056

merged 55 commits into from
Mar 13, 2024

Conversation

EgbertRijke
Copy link
Collaborator

The changes in this PR are pulled from #885.

@EgbertRijke EgbertRijke marked this pull request as draft March 5, 2024 13:38
@EgbertRijke
Copy link
Collaborator Author

Yay this actually compiles now:)

@fredrik-bakke
Copy link
Collaborator

Congrats! 🎉🎉🎉
I assume @VojtechStep perhaps wants to review this, so I'll hold off on starting a review until I see him.

@EgbertRijke
Copy link
Collaborator Author

Sure!

Note that this PR itself doesn't have much to do with synthetic homotopy, other than that the changes made here are in preparation for the refactoring of our treatment of pointed pushouts.

VojtechStep
VojtechStep reviewed Mar 7, 2024
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

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

Great work! Thanks for splitting this out of that big PR. I still have 6 files to review, but I'll do that some other time, hopefully tomorrow.

src/structured-types/pointed-homotopies.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-homotopies.lagda.md Show resolved Hide resolved
src/structured-types/pointed-homotopies.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-homotopies.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-homotopies.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-equivalences.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-equivalences.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-equivalences.lagda.md Outdated Show resolved Hide resolved
src/structured-types/commuting-squares-of-pointed-maps.lagda.md Outdated Show resolved Hide resolved
src/structured-types/commuting-squares-of-pointed-maps.lagda.md Outdated Show resolved Hide resolved
@EgbertRijke EgbertRijke marked this pull request as ready for review March 9, 2024 10:48
@EgbertRijke
Copy link
Collaborator Author

I have cut off all the unfinished parts of morphisms-pointed-arrows and declare this pull request ready for review. I got to extensionality of morphisms of pointed arrows, and that was a natural point to stop.

@EgbertRijke
Copy link
Collaborator Author

I am now done with my revisions based on the review comments.

VojtechStep
VojtechStep reviewed Mar 9, 2024
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

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

Thanks for the rewording and explanations. I finished reviewing the PR; there's no rush to address the comments

src/structured-types/constant-pointed-maps.lagda.md Outdated Show resolved Hide resolved
src/structured-types/morphisms-pointed-arrows.lagda.md Outdated Show resolved Hide resolved
src/structured-types/morphisms-pointed-arrows.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-2-homotopies.lagda.md Outdated Show resolved Hide resolved
src/structured-types/pointed-2-homotopies.lagda.md Outdated Show resolved Hide resolved
src/structured-types/whiskering-pointed-homotopies-composition.lagda.md Outdated Show resolved Hide resolved
src/structured-types/whiskering-pointed-homotopies-composition.lagda.md Outdated Show resolved Hide resolved
src/structured-types/whiskering-pointed-homotopies-composition.lagda.md Outdated Show resolved Hide resolved
src/structured-types/whiskering-pointed-homotopies-concatenation.lagda.md Outdated Show resolved Hide resolved
src/structured-types/whiskering-pointed-homotopies-concatenation.lagda.md Outdated Show resolved Hide resolved
@VojtechStep VojtechStep mentioned this pull request Mar 13, 2024
Open
@VojtechStep
Copy link
Collaborator

Everything looks great, I'm hitting the green button 👌

@VojtechStep VojtechStep enabled auto-merge (squash) March 13, 2024 16:56
@VojtechStep VojtechStep merged commit 6065e29 into UniMath:master Mar 13, 2024
4 checks passed
fredrik-bakke pushed a commit to fredrik-bakke/agda-unimath that referenced this pull request Mar 14, 2024
@EgbertRijke @fredrik-bakke
Refactoring pointed types (UniMath#1056)
e32e305 
The changes in this PR are pulled from UniMath#885.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@VojtechStep VojtechStep VojtechStep left review comments

@fredrik-bakke fredrik-bakke fredrik-bakke left review comments

Assignees
No one assigned
Labels
refactoring structured-types
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@EgbertRijke @fredrik-bakke @VojtechStep