lax/oplax/pseudo-trans between lax/oplax/pseudo-functors

Stream: mathlib4

[Yuma Mizuno]

We (at least @Calle Sönne, @Robin Carlier, and I) are recently formalizing the notation related to functor bicategories (e.g., #14089 and #25565).

Actually, there are 3^2 possibilities on what we think of functor bicategories: considering {lax/oplax/pseudo}-natural transformations between {lax/oplax/pseudo}-functors, depending on the treatment of 2-cells.

As a non-expert in this field, I think the following notions are natural and worth formalizing in mathlib:

• lax transformations between lax functors (open PR #25779)
• lax transformations between oplax functors (open PR #25825)
• oplax transformations between lax functors (open PR #25825)
• oplax transformations between oplax functors (already in mathlib)
• pseudonatural transformation between pseudofunctors (already in mathlib)

However, I'm not sure for other four cases. In these cases we have iso and hom simultaneously, which seems a bit inconsistent.

I would be grateful if anyone with familiar with this topic (or anyone having ideas) could provide a comment.

[Calle Sönne]

what do you mean by "we have iso and hom simultaneously"? If I've understood it correctly, a strong/pseudonatural transformation between oplax functors does not give an oplax transformation which is an isomorphism.

[Yuma Mizuno]

I mean using hom for functor (mapId and mapComp) whereas using iso for natural transformation (naturality), or vice versa.

[Robin Carlier]

I also think that it feels more "natural" to have pseudofunctors and their (strong) natural transformations have Iso everywhere.

For strong natural transformations between op/lax functors, perhaps we could make a class IsStrong on op/lax natural transformation that says that the relevant 2-cells have an IsIso instance? This way, we can still have the notion, while keeping things somewhat coherent?
The only issue I might see with this approach is that if we prove that an IsStrong lax transformation of lax functors defines an IsStrong oplax transformation of lax functors (I think this is true? We just take the inverse 2-cell everywhere), then if we apply the same kind of construction to get back an IsStrong lax nat. trans. we probably won't have a defeq between this and the original nat. trans.

I'm also not so sure where they arise in nature, and to me the argument to have them is "for the sake of completeness".
One example I can see in which they might appear is the following: When we see lax monoidal functors as lax natural transformations between 1-object bicategories, I think strong transformations correspond to natural isomorphisms of lax functors, but that's also a statement in which we can phrase everything as IsIso (at least if we're fine with noncomputable) and potentially we don't need to develop the whole general theory of strong transforms of lax functors for this.

[Yuma Mizuno]

Robin Carlier said:

One example I can see in which they might appear is the following: When we see lax monoidal functors as lax natural transformations between 1-object bicategories, I think strong transformations correspond to natural isomorphisms of lax functors, but that's also a statement in which we can phrase everything as IsIso (at least if we're fine with noncomputable) and potentially we don't need to develop the whole general theory of strong transforms of lax functors for this.

For monoidal case, the situation is simplified as we can just put properties for (usual) natural transformations between (usual) functors underlying lax monoidal functors: docs#CategoryTheory.NatTrans.IsMonoidal.

[Yuma Mizuno]

Robin Carlier said:

For strong natural transformations between op/lax functors, perhaps we could make a class IsStrong on op/lax natural transformation that says that the relevant 2-cells have an IsIso instance? This way, we can still have the notion, while keeping things somewhat coherent?

Perhaps docs#CategoryTheory.Oplax.OplaxTrans.StrongCore is the data carrying version of that?

[Robin Carlier]

I have submitted #25760 today, that defines oplax natural transformations between lax functors. The reason for this sudden push is that I expect that these transformations will be the basis of the definitions of icons (short for "identity component oplax natural transformations"), which can be used tho define a strict 2-category of bicategories.

(Icons are "evil", because by definition an icon from F to G bundles an equality F.obj x = G.obj x for every x, but these are still desirable as the strict 2-category of bicategories, strictly unitary pseudofunctors and icons between those is the natural domain of Lack-Paoli’s 2-nerve, see Johnson-Yau, section 5.5)

[Yuma Mizuno]

Is the PR #27903?

[Yuma Mizuno]

I also defined

• oplax transformations between lax functors
• lax transformations between oplax functors

in #25825, but depending on your open PR #25779 that has not yet been merged. Sorry for not following up on this in this thread.

[Robin Carlier]

Oh right, I keep being bad at copy-pasting numbers. The number is #27903 indeed!

I forgot about #25825, I'll close #27903 then (it wasn't very long to make anyways, mostly copy-pasting)

[Yuma Mizuno]

I'm curious to see how the evilness of icons turns out. Will there be a lot of eqToHom handling at some point?

[Robin Carlier]

My first experiments is that yeah, we'll have to deal with some eqToHoms, and also compositions of such: in a bicategory, I don't this we can hope that eqToHom (p.trans q) = (eqToHom p).comp eqToHom q holds. For the definition of icons it's not an issue, but it pops up already for the fact that they compose well... I didn't run in coherences issues with this yet, but my experiments are not very advanced yet.

[Robin Carlier]

The definition of icons is at #28244

[Robin Carlier]

Strictness of their composition is at #28245.

[Yuma Mizuno]

It looks that #25779 is currently marked as awaiting author.
@Robin Carlier When you have a chance, could you please take a look at it?

[Robin Carlier]

Sure, sorry I’m very behind on fixing basically all of my open PRs. I should be able to look at it by this evening.

[Yuma Mizuno]

No problem at all! I really appreciate it, and there’s absolutely no rush.