1lab icon indicating copy to clipboard operation
1lab copied to clipboard

Add definitions for preservation/reflection of specific (co)limits

Open TOTBWF opened this issue 3 years ago • 1 comments
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.

TOTBWF avatar May 17 '22 16:05 TOTBWF

Note that this would involve refactoring the definition of is-lex in Cat.Diagrams.Limit.Finite to use the new predicates.

plt-amy avatar May 17 '22 17:05 plt-amy