Stream: Is there code for X?

Topic: has_limits of has_limits and creates_limits

Adam Topaz (Sep 24 2020 at 02:14):

Is there a way to make the following work?

import category_theory.limits.creates

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 (Sep 24 2020 at 02:26):

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 (Sep 24 2020 at 03:02):

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 (Sep 24 2020 at 03:29):

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

Adam Topaz (Sep 24 2020 at 03:30):

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

Bhavik Mehta (Sep 24 2020 at 14:14):

Yeah I agree this should be there as a def

Adam Topaz (Sep 24 2020 at 14:26):

@Bhavik Mehta @Scott Morrison #4239

Last updated: May 07 2021 at 22:14 UTC