Add (co)products #637
Add (co)products #637
Conversation
|
See how I just refactored the pullbacks: #650 |
|
@mortberg could you be more specific please? I'm not sure what exactly you'd like me to do - I think my code already looks pretty similar to your refactored code. |
|
State the universal property first just as a definition and not as a record and then prove that it's a property. Then use it to define the product/equalizer structure. Finally, give a definition of what it means for a category to have and merely have products/equalizers: https://github.com/agda/cubical/pull/650/files#diff-9d881e0b34956b31c18090a3faa7d4b14e7adea7aa927fd6914a2ea2cc839ae8R53 |
|
Great, I can do that. |
Perfect! Just so you know: I plan to rewrite the file about terminal objects and limits soon as well. |
|
Cool. Just so you know, I defined coproducts and coequalisers too (as products/equalisers in the opposite category) and was planning to PR them after this one got approved. |
|
I actually don't think it's good to define colimits as limits in C^op. This leads to more headache than its worth (for example record projections will have the wrong names, e.g. the maps into the coproduct will be called projections...). My experience from UniMath is that it's much better to define all limits and colimits as directly as possible. It's also kind of arbitrary that the colimits are limits in C^op, we could just as well take colimits as primitive and define limits as colimits in C^op. No matter what it's better to keep them separate |
|
@mortberg have refactored to match your code. I removed equalisers since I don't need them for what I'm doing, and added coproducts. |
Sadly I won't have time to put that together, but it should be easy enough to copy the structure of these files. |
Ok, no problem! I'll do it myself |
No description provided.