1lab
1lab copied to clipboard
Add definitions for preservation/reflection of specific (co)limits
trafficstars
Right now we have a notion of preservation/reflection of (co)limits that works over limit diagrams, but this is often a bit annoying to work with when we are working with some concrete (co)limit, as it involves dancing between limit diagrams + the concrete definitions. It would be a bit more ergonomic if we had some definitions like Preserves-products or Reflects-coequalisers, as well as a good API for moving between the general + specific forms.
Note that this would involve refactoring the definition of is-lex in Cat.Diagrams.Limit.Finite to use the new predicates.