isomorphism of functors

Stream: Is there code for X?

[Aaron Liu]

Is there a way to say two functors are isomorphic? That is, given two functors F and G I want the type of natural isomorphisms between F and G. This is talking about docs#LawfulFunctor, not those category-theory functors. Ideally I would want this to be as universe-polymorphic as possible, so the domain and codomain of F and G can be four different universes (I guess if they're in different universes this would be saying the one functor naturally extends the other functor into the higher universe).

[Yaël Dillies]

Have you considered turning the Type functors into category theory functors, then use categorical isomorphisms?

[Aaron Liu]

that sound like a lot of work and also not universe polymorphic

[Yaël Dillies]

I agree, but whether universe polymorphism is worth fighting for depends on your application: What's your application?

[Yaël Dillies]

To be clear, my suggestion works today:

[Aaron Liu]

For defining CGT#GameFunctor

[Yaël Dillies]

@loogle Functor, CategoryTheory.Functor

[Aaron Liu]

well not the definition but using the fact that it's a quotient of a polynomial functor

[Yaël Dillies]

Can you clearly say what two functors you want to state are isomorphic?

[Aaron Liu]

The CGT#GameFunctor and the quotient of the polynomial functor in the QPF instance we put on it

[Aaron Liu]

across all the universes

[Yaël Dillies]

Great, but can you give their types? I see GameFunctor : Type (u + 1) -> Type (u + 1). What about the other one?

[Matt Diamond]

not sure why loogle didn't work above but I'm guessing Yael was trying to surface docs#CategoryTheory.ofTypeFunctor

[Aaron Liu]

probably I think it will be Type v -> Type (max v (u + 1))

[Matt Diamond]

ofTypeFunctor seems to support universe polymorphic functors? but I could be misreading it

[Aaron Liu]

Yaël Dillies said:

@loogle Functor, CategoryTheory.Functor

@loogle Functor, CategoryTheory.Functor

[loogle]

:search: CategoryTheory.ofTypeFunctor

[Matt Diamond]

yeah, that's what I thought

[Aaron Liu]

Matt Diamond said:

ofTypeFunctor seems to support universe polymorphic functors? but I could be misreading it

But surely we don't support natural isomorphisms between functors with different source/target categories

[Aaron Liu]

so if I have a functor Type u -> Type v and another one Type u' -> Type v' then I don't expect to be able to state that they're compatible using the category theory machinery since they're different types

[Matt Diamond]

you're probably right but I would confirm by looking at docs#CategoryTheory.Functor.category, which is what you end up doing the iso in

[Matt Diamond]

yeah that's true, C and D are fixed

[Matt Diamond]

alright yeah, not universe polymorphic then

[Christian Merten]

The battle tested way is to suitably compose with docs#CategoryTheory.uliftFunctor.

[Aaron Liu]

then I have ulifts everywhere

[Aaron Liu]

I guess it's not impossible to work with

[Aaron Liu]

so now I have to import category theory too?

[Yaël Dillies]

Why do you need universes? Is it not enough to talk about your second functor when v := u + 1?

[Aaron Liu]

For coinduction it took a lot of effort to make it universe polymorphic

[Aaron Liu]

so I'm thinking can I upstream some of this into QPF but then this requires refactoring it to be bundled

[Aaron Liu]

so I want to say that the bundled QPF is iso to the nicer description

[Yaël Dillies]

What do you want to do with the isomorphism? What is its envisioned application?

[Aaron Liu]

Transfer the coinduction principle across it

[Aaron Liu]

I guess another perspective would be transfer the cofixpoint across

[Aaron Liu]

The one functor has a terminal coalgebra so the other functor also does since it's isomorphic

[Aaron Liu]

oh and probably the same thing dually for the initial algebra

[Yaël Dillies]

So do you really need a way to state the isomorphism? Why don't simply write down the natural transformation by hand both ways?

[Aaron Liu]

That's the plan

[Aaron Liu]

I was hoping there would be a way to write lemmas about this though

[Aaron Liu]

lemmas which don't only apply to my one specific natiso

[Yaël Dillies]

This seems to be a niche enough application that writing one off lemmas seems fine

[Aaron Liu]

Christian Merten said:

The battle tested way is to suitably compose with docs#CategoryTheory.uliftFunctor.

I don't think that works, because the source categories are also in different universes, and ulift only lifts up so the direction of composition means I can only push these source universes down, which loses information about what happens to big types

[Aaron Liu]

there's also no good candidate for which universe I would descend to, there's no universe min like there is a max