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

Show that conservative functors reflect specific (co)limits

Open TOTBWF opened this issue 3 years ago • 0 comments

Right now, we have proofs that conservative functors reflect all limits that they preserve, but using this result is a bit annoying as we have to mediate between concrete (co)limits and their (co)limit diagrams. It would be nice if we did something analogous to Cat.Functor.Adjoint.Continuous and provide results specialized to concrete (co)limits.

This is blocked on #82 and #76.

TOTBWF avatar May 17 '22 16:05 TOTBWF