Skip to content

Clean up cubical primitives #6034

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
Merged
merged 5 commits into from
Aug 18, 2022
Merged

Clean up cubical primitives #6034

merged 5 commits into from
Aug 18, 2022

Conversation

plt-amy
Copy link
Member

@plt-amy plt-amy commented Aug 18, 2022

Step one in my evil plan to replace abuses of the interval by a proper cofibration classifier is to clean up all the Cubical Agda primitives. Here's ~60% of them.

@plt-amy plt-amy added type: enhancement Issues and pull requests about possible improvements type: task Concerning the development of Agda (not in changelog) cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp labels Aug 18, 2022
@plt-amy plt-amy self-assigned this Aug 18, 2022
andreasabel
andreasabel approved these changes Aug 18, 2022
View reviewed changes
Copy link
Member

@andreasabel andreasabel left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Thanks!
As this PR has lots of code movement, I cannot sensibly review the changes.
Where I could, I gave some minor stylistic comments.

@plt-amy plt-amy merged commit 503a9bd into master Aug 18, 2022
@plt-amy plt-amy deleted the aliao/cubical-clean-up branch October 27, 2022 13:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@plt-amy plt-amy

Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp type: enhancement Issues and pull requests about possible improvements type: task Concerning the development of Agda (not in changelog)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@plt-amy @andreasabel