Zulip Chat Archive

Stream: Is there code for X?

Topic: functors and universe constraints

view this post on Zulip Kyle Miller (Feb 18 2021 at 00:40):

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.)

view this post on Zulip Bhavik Mehta (Feb 18 2021 at 15:58):

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)

view this post on Zulip Bhavik Mehta (Feb 18 2021 at 16:01):

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.

view this post on Zulip Bhavik Mehta (Feb 18 2021 at 16:03):

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

view this post on Zulip Bhavik Mehta (Feb 18 2021 at 16:04):

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

view this post on Zulip Kyle Miller (Feb 19 2021 at 21:38):

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)

view this post on Zulip Kyle Miller (Feb 19 2021 at 21:46):

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

view this post on Zulip Bhavik Mehta (Feb 19 2021 at 22:59):

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:

view this post on Zulip Bhavik Mehta (Feb 19 2021 at 23:07):

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

view this post on Zulip Scott Morrison (Feb 20 2021 at 09:35):

Someone should PR it!

Last updated: May 16 2021 at 05:21 UTC