Stream: maths

Topic: Creating limits extends reflects limits?

Bhavik Mehta (May 10 2020 at 16:52):

Some time ago my PR for creating limits got merged to mathlib, and I'm trying to use it. In particular, here I define creates_limit to extend reflects_limit, and then generalise to creates_limits_of_shape etc. Now I have a functor which I know creates_limits_of_shape walking_cospan and I expected that it should reflects_limits_of_shape walking_cospan, but this isn't automatic at the moment. My question now is: should the definition of creates_limits_of_shape extend reflects_limits_of_shape? Or should there be an instance giving this instead?

Last updated: May 06 2021 at 19:30 UTC