functors and universe constraints

Stream: Is there code for X?

[Kyle Miller]

I have a very clumsy construction that takes a functor between categories of different universes, makes a functor between new categories of the same universe (via ulift), applies a lemma for such functors, then lowers the result down into the original universes. I'm sure there must be a better way than what I have: #6288

(I'm also wondering what the reason is for Top.limit_cone requiring functors to be between categories of the same universe -- if there weren't this constraint, then the above complexity would go away.)

[Bhavik Mehta]

All of the constructions about limits and cones require the indexing category to have its objects and homs in the same universe as the homs of the category C - combined with the fact that Top is a large category, this is the reason for the universe restrictions you mention. I'm working on a branch which relaxes this restriction (it turns out that most of the time you don't need it at all)

[Bhavik Mehta]

In this specific case though, F.sections is a sigma type, so its universe is the maximum of the universe of the objects of both categories, so if they're different then the type F.sections will live in a higher universe than you started with (this is problematic if you naively try to take a Type v indexed limit in Type u, where the limit ends up being in Type (max u v) and hence might not exist in your original category) so for this it would make sense to have u = v.

[Bhavik Mehta]

All that said, there are cases when certain "large" limits do exist, even if the construction F.sections is too big too fit, so there could be constructions saying something like, if c is a cone over your (not necessarily small) directed order, and it happens to be a limiting cone (plus the finite+nonempty stuff you assumed) then the apex of the cone is nonempty too

[Bhavik Mehta]

The distinction here is that I'm not assuming F.sections is the limit object, instead saying that if you give me any limit object and tell me it's a limit, then I can tell you it's nonempty

[Kyle Miller]

Thanks for the information @Bhavik Mehta. It makes a good amount of sense to set things up for categorical constructions.

(A couple of weeks ago I tried out a variation on categories where the homomorphism class is indexed by the objects:

class HasHom {α β : Type*} (x : α) (y : β) := (Hom : Type*)

This lets you have homomorphisms between things even if there's no formal "category" object that encompasses everything under consideration -- for example this lets you use the same notation for functors as for other homomorphisms. It all seems to be rather unwieldy to use (and you can end up with some absurdly large type signatures), but it's sort of interesting because it would let you do things like have hom sets between topological spaces themselves, rather than needing to wrap the spaces up as terms of Top. I just thought I'd share since it's vaguely related, and I'm definitely not recommending that we change anything! https://gist.github.com/kmill/7da8de685e602917dc939ec768d0f26c)

[Kyle Miller]

Related to that (and still related to the topic of functors), I had a hard time writing down the S combinator as a functor. The library already has the I and K combinators, and if we had S then we could mechanically turn lambda expressions into their functor versions. Does this already exist somewhere? or does someone have more fortitude than myself to write it?

lemma Functor.S {α β γ : Type*} [category α] [category β] [category γ] :
  (α ⥤ β) ⥤ (α ⥤ β ⥤ γ) ⥤ α ⥤ γ := sorry

[Bhavik Mehta]

def diag {α : Type*} [category α] :
  α ⥤ α × α :=
{ obj := λ X, ⟨X, X⟩,
  map := λ X Y f, ⟨f, f⟩ }

def Functor.W {α β : Type*} [category α] [category β] :
  (α ⥤ α ⥤ β) ⥤ (α ⥤ β) :=
uncurry ⋙ (whiskering_left _ _ _).obj diag

def Functor.B {α β γ : Type*} [category α] [category β] [category γ] :
  (β ⥤ γ) ⥤ (α ⥤ β) ⥤ α ⥤ γ :=
whiskering_right α β γ

def Functor.C {α β γ : Type*} [category α] [category β] [category γ] :
  (α ⥤ β ⥤ γ) ⥤ (β ⥤ α ⥤ γ) :=
{ obj := functor.flip,
  map := λ F G t,
  { app := λ X,
    { app := λ Y, (t.app Y).app X,
      naturality' := λ Y Y' f, nat_trans.naturality_app _ _ _ } } }

def Functor.S {α β γ : Type*} [category α] [category β] [category γ] :
  (α ⥤ β) ⥤ (α ⥤ β ⥤ γ) ⥤ α ⥤ γ :=
functor.flip ((Functor.B.obj (Functor.B.obj Functor.W)).obj ((Functor.B.obj Functor.B).obj Functor.C))

This works :upside_down:

[Bhavik Mehta]

Even better would be to show Cat is cartesian closed and construct these combinators in any cartesian closed category

[Scott Morrison]

Someone should PR it!