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

Path-cosplittings of locally small types are locally small #1251

Merged
merged 7 commits into from
Jan 31, 2025

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Jan 30, 2025

Shows that locally small types are closed under path-cosplittings.

@fredrik-bakke
Copy link
Collaborator Author

Ah, shoot, I made this branch on the wrong fork

@fredrik-bakke
Copy link
Collaborator Author

Sorry about that

@EgbertRijke
Copy link
Collaborator

Looks good to me!

Is it still on the wrong branch or can it be merged?

@fredrik-bakke
Copy link
Collaborator Author

Looks good to me!

Is it still on the wrong branch or can it be merged?

Thanks! No, this one can be merged. I already tidied up everything that needed to be tidied. There will be some merging work for me to do later with some of the PRs that are marked as drafts, but each of my PRs that is marked as ready for review is also ready to be merged in my books.

@fredrik-bakke fredrik-bakke enabled auto-merge (squash) January 31, 2025 20:22
@fredrik-bakke
Copy link
Collaborator Author

Oh, you mean the thing about the fork. Yeah, this branch is on the wrong fork. I will delete it after. Sorry

@fredrik-bakke fredrik-bakke merged commit 57119df into master Jan 31, 2025
4 checks passed
@fredrik-bakke fredrik-bakke deleted the retract-locally-small branch January 31, 2025 20:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants