-
Notifications
You must be signed in to change notification settings - Fork 70
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
Postulating colimits #1122
Comments
Would it make sense to add "postulate spheres" to the To Do list? They can be inductively defined as suspensions. But this could also just be a theorem. The more straight forward definition would be the point and n loop definition. Plus this matches the definition of the circle. |
Indeed it should also include the spheres. However, changing the underlying presentation is a separate issue. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
It seems to me that the most principled approach to adding colimits to the library through postulates is to postulate their individual existence, their dependent eliminator, and its computation rules, and to show everything else from this. In particular, if their existence follows from the existence of some other type of colimit, then that should be a theorem rather than a definition. This avoids deciding on a preferred "main" type of colimit, from which other types of colimits should be defined, also avoiding awkward module dependencies. Another benefit of this approach is that it gives us finer-grained control over rewrite rules. For instance, if one wants to enable rewrite rules for joins, it shouldn't be necessary to enable rewrite rules for all pushouts.
TODO
The text was updated successfully, but these errors were encountered: