Skip to content

various improvements to wedge #1849

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

Merged
merged 2 commits into from
Feb 13, 2024

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Feb 12, 2024

These are some quality of life improvements for working with wedges. They consist of:

  • Adding explicit universe levels for wedges. Not sure if they need to be generalised further. I've opted for 2 levels for the source and target. I can't tell if having 3 will be useful at this point. Universe levels are generalized correctly now.
  • Generalising wedge_rec to target any type (in any universe) and naming that wedge_rec'. Then redefining wedge_rec as a special case of wedge_rec'.
  • Using wild category notations for various arrows and homotopies so that fmap and friends work better.
  • Add a computation rule for the wedge inclusion.

@Alizter Alizter force-pushed the ps/branch/various_improvements_to_wedge branch from 4fbf855 to b73b162 Compare February 12, 2024 21:37
@Alizter Alizter force-pushed the ps/branch/various_improvements_to_wedge branch from b73b162 to ae6caa6 Compare February 13, 2024 00:02
@jdchristensen
Copy link
Collaborator

LGTM.

@Alizter Alizter merged commit 697cac9 into HoTT:master Feb 13, 2024
@Alizter Alizter deleted the ps/branch/various_improvements_to_wedge branch February 13, 2024 00:35
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