has_limits of has_limits and creates_limits

Stream: Is there code for X?

[Adam Topaz]

Is there a way to make the following work?

import category_theory.limits.creates
import category_theory.monad.limits

open category_theory

universes u v
variables (C D : Type u) [category.{v} C] [category.{v} D]
variables (F : C ⥤ D)
variables [limits.has_limits D] [creates_limits F]

example : limits.has_limits C := by apply_instance -- fails

[Adam Topaz]

I know I can't expect typeclass search to work, since it has no way of knowing about F, but I would be happy with a def that I can use for the example.

[Adam Topaz]

Okay, I completed the example with the following:

example : limits.has_limits C :=
⟨λ J I, by letI := I; exact ⟨λ G, has_limit_of_created G F ⟩⟩

Is this in mathlib somewhere?

[Scott Morrison]

Not to my knowledge! Shims like this are definitely useful.

[Adam Topaz]

I'm playing with it now. It works out well too, e.g. the functor F automatically gets a preserves_limits instance.

[Bhavik Mehta]

Yeah I agree this should be there as a def

[Adam Topaz]

@Bhavik Mehta @Scott Morrison #4239