1lab
1lab copied to clipboard
Show that conservative functors reflect specific (co)limits
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.