Universes and sheaves

Stream: maths

[Adam Topaz]

Our definition of docs#category_theory.Sheaf has the following universe restriction, which seems too restrictive to me: Given C : Type u with category.{v} C and grothendieck topology Ton C, we can define A-valued sheaves on C (w.r.t. T) provided A : Type u' has a category.{v} A.

Is there a good reason why the universe level of morphisms for C is required to be the same as the one for A?

[Bhavik Mehta]

Perhaps not - I recall trying to make the universes as un-restricted as possible (without resorting to ulift), but this might have been one of the cases where the universe level of Sheaf J and its morphisms look very ugly if they're different.

[Bhavik Mehta]

Oh actually, looking at this again, coyoneda is the one which insists on the universe restrictions, in is_sheaf. Can you lift the universe-level of the morphisms for your case?

[Adam Topaz]

I see. coyoneda does indeed impose this restriction. I would have to think more carefully about what I actually want.

The main thing that seems silly to me, in the context of condensed sets, is that as_small.{u+1} Profinite.{u} \func Type (u+1) is equivalent to Profinite.{u} \func Type (u+1). Adding the as_small stuff just introduces some seemingly unnecessary complexity.

[Bhavik Mehta]

I agree - the distinction is in the statement of the sheaf condition

[Adam Topaz]

I tracked down the issue to docs#category_theory.sieve.functor and docs#category_theory.presieve.yoneda_sheaf_condition