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

Clear Up Fillers #1061

Open
wants to merge 25 commits into
base: master
Choose a base branch
from
Open

Clear Up Fillers #1061

wants to merge 25 commits into from

Conversation

kangrongji
Copy link
Contributor

@kangrongji kangrongji commented Sep 21, 2023

This PR reorganizes the cube fillers in library. They've been renamed uniformly, deduced as corollaries of the extend operation and now collected in Cubical.Foundations.HLevels.Fillers. There are still some left in Cubical.Foundations.Prelude due to their preliminary nature. @mortberg

To achieve this, I have to separate the basic definitions and facts about h-levels from Cubical.Foundations.HLevels into a new file Cubical.Foundations.HLevels.Base. Additionally, I separated the cube types in Cubical.Foundations.Prelude to the file Cubical.Foundations.Cubes.

@kangrongji kangrongji marked this pull request as ready for review September 22, 2023 05:11
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.

1 participant