Trying to infer instance with argument

Stream: new members

[Jack J Garzella]

As part of #maths > Definition of presheaf of modules , I'm trying to use that the category of sheaves of types is monoidal. I'd like to get lean to synthesize the instance using monoidal_of_has_finite_products. However, I seem unable to avoid the following issue: the instance for (Sheaf J D) having finite limits assumes that D has finite limits, see here.

I can't seem to get lean to figure out how to infer this, even if I use the have tactic to move the instance to the context. However, if I assume that sheaves have limits, Lean can do the rest.
Does someone know the correct way to do this?

The #mwe:

import category_theory.sites.sheaf
import category_theory.monoidal.Mon_
import category_theory.closed.cartesian
import category_theory.sites.limits
import category_theory.limits.has_limits

open category_theory
open category_theory.limits
open category_theory.Sheaf.category_theory.limits

universes u v w

variables {C : Type u} [category.{v} C] {J : grothendieck_topology C}


lemma type_has_limits : has_limits (Type w) := ⟨⟩
lemma sheaves_have_limits : has_limits (Sheaf J (Type w)) :=
begin
  have h := type_has_limits,
  exact (infer_instance : has_limits (Sheaf J (Type w)))
end

variables [hw : has_limits (Sheaf J (Type w))]
include hw
#check monoidal_of_has_finite_products (Sheaf J (Type w))

[Reid Barton]

There is almost certainly some universe issue here

[Reid Barton]

I'm not sure why the universes in category_theory.sites.limits are set up in such a complicated way; maybe @Adam Topaz knows?

universes w v u
variables {C : Type (max v u)} [category.{v} C] {J : grothendieck_topology C}
variables {D : Type w} [category.{max v u} D]

[Reid Barton]

For colimits, of course we will need some specific assumptions--maybe that's the reason?

[Adam Topaz]

There was a universe restriction (which may have been resolved? I don't know) in limits/colimits of functors, and this the choice for sheaves was made so that we could use limits and colimits of functors.

[Reid Barton]

Sheaves themselves seem to have fully general universes

[Adam Topaz]

That's right, the category of sheaves is completely universe polymorphic

[Adam Topaz]

The heart of the issue is the universe level of morphisms of (pre)sheaves, which involves the universe level of C, the universe level of the morphisms of C and the universe level of the morphisms of the target of the presheaves

[Reid Barton]

@Jack J Garzella This specialization of universes will work:

universes u v

variables {C : Type (max v u)} [category.{v} C] {J : grothendieck_topology C}
#check monoidal_of_has_finite_products (Sheaf J (Type (max v u)))

[Adam Topaz]

The easiest case is when your C is a small category, then you just have to match the universe level of the morphisms of your target category with the universe level of C.

[Adam Topaz]

These universe gymnastics were done so that we could talk about sheaves on Profinite.{u}, which is a large category

[Adam Topaz]

We could try to generalize the universe parameters for limits, but for colimits you need to sheafify, and that gets more complicated.

[Reid Barton]

Oh right I see now, Sheaf J W has whatever limits W has, but its morphisms might live somewhere bigger

[Adam Topaz]

It seems that the universe parameters for (co)limits of functors have been generalized, so something can probably be done for sheaves as well (assuming someone has enough energy)

[Reid Barton]

In particular, Sheaf J W could inherit has_finite_limits from W without any universe assumptions

[Adam Topaz]

There was a very recent change where all finite (co)limits have their diagrams in Type 0.

[Jack J Garzella]

So, if I change the {C : Type (max v u)} in @Reid Barton 's code to {C : (max u v)}, the code no longer works (whether or not the u and v are swapped in the last line does not affect this). Is there any reason why it should work this way?

[Reid Barton]

Sort of. Lean has to infer what universe levels to instantiate the has_limits instance at and apparently it starts out by unifying the universe of C, so max ?v ?u = max v u is solved by setting ?v = v, ?u = u. One could imagine other strategies that would do better here.

[Reid Barton]

This is why putting a universe expression in the type of an argument that is more complicated than a single variable can be quite annoying at the use site