Postulating colimits

[fredrik-bakke]

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

• [ ] Postulate sequential colimits
• [ ] Postulate coequalizers
• [ ] Postulate joins
• [ ] Postulate suspension
• [ ] Postulate spheres
• [ ] Split induction principle for circle into dependent eliminator and computation rule
• [ ] Add rewriting files for each family of colimit

[morphismz]

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.

[fredrik-bakke]

Indeed it should also include the spheres. However, changing the underlying presentation is a separate issue.