can bicategory infrastructure be applied to Cat?

Stream: mathlib4

[Emily Riehl]

On the face of it, the question in the title may sound stupid, but let me explain why I think it's not. Whether or not it's stupid, I'd like to know the answer.

By bicategory stuff, I'm thinking in particular about this cleverly designed CategoryTheory.bicategoricalComp and CategoryTheory.bicategoricalIsoComp operations defined here that @Yuma Mizuno defined for 2-cells or invertible 2-cells:

def CategoryTheory.bicategoricalComp{B : Type u} [Bicategory B]
{a b : B} {f g h i : a ⟶ b} [BicategoricalCoherence g h]
(η : f ⟶ g) (θ : h ⟶ i) : f ⟶ i

It applies in a setting where you have a pair of 2-cells η and θ that are morally composable but not actually composable, since the codomain g of η is related to the domain h of θ by a bicategorical coherence (something built out of associators and unitors) but these are not actually equal.

Note you can apply this in the context of any bicategory and we have CategoryTheory.Cat.bicategory giving a bicategory instance on Cat, so surely we can apply this to categories, functors, and natural transformations?

I was thinking of this question when @Sophie Morel showed us some of the formalizations she's done such as the definition of DerivedFunctor_comp. The annoying part of the proof is in constructing an explicit natural isomorphism (an invertible 2-cell in Cat) and I'm wondering if bicategoricalIsoComp can be used to avoid some of the named coherences?

My guess is no not directly due to issues with

(i) universes; technically the bicategory structure lives on Cat.{v,u} for fixed universes u and v
(ii) conflicting notation for functors and morphisms in Cat and natural transformations and 2-cells in Cat.

We described this sort of issue in a recent preprint.

If this can't be done now, could it conceivably be in the future? If it can, please teach me (and @Sophie Morel) how to simplify proofs like this.

[Robin Carlier]

Note that with categories and functors, all "named coherences" (i.e associators and unitors) are in fact Iso.refl _, so you could in fact just put (Iso.refl : <expected type>) everywhere, and it’d "just" work, even worse, you could even skip them and for some compositions it’d work... For this kind of things, this is a bit of a "bug", because Lean will actually accept Functor.rightUnitor F as an isomorphism 𝟭 _ ⋙ F ≅ F!

That being said, I had a go at simply copy-pasting the code in BicategoricalCoherence, replacing every instance of a 1-cell by a functor, and it "just works", you can play with it here. At the end of the day, @Yuma Mizuno's code for bicategorical (and monoidal) composition does not rely on any "coherence" tactics, but rather on a clever use of the type class system, letting lean infer that the two sides of the compositions "are related by a coherence 2-cell".
But again, every single iso appearing here is Iso.refl _, and all ⊗≫ is doing in the link I gave is inserting some identities that are "well-typed" to help lean.

[Yuma Mizuno]

By the way, the code for ⊗≫, which was originally written for monoidal categories, should be credited to @Kim Morrison , not me.

[Notification Bot]

6 messages were moved from this topic to #mathlib4 > Functor identity `𝟭 _ ⋙ F = F` is definitional equality by Yuma Mizuno.

[Yuma Mizuno]

Emily Riehl said:

On the face of it, the question in the title may sound stupid, but let me explain why I think it's not. Whether or not it's stupid, I'd like to know the answer.

The tactic docs#CategoryTheory.to_app by @Calle Sönne is a tool that applies bicategory infrastructure to Cat. It provides equalities in Cat after applying natural transformations to objects.

[Yuma Mizuno]

example

[Yuma Mizuno]

Emily Riehl said:

(i) universes; technically the bicategory structure lives on Cat.{v,u} for fixed universes u and v
(ii) conflicting notation for functors and morphisms in Cat and natural transformations and 2-cells in Cat.

There are two possible formulation for declaring C and D are categories:

variable (C : Type u1) (D : Type u2) [Category.{v1} C] [Category.{v2} D]

and

variable (C D : Cat.{v, u})

The to_app is for the latter setting, so doesn't address these points.

[Yuma Mizuno]

When we working on the latter (Cat) setting, we can use bicategory structure at any time. So the tool we would like to have is one generating the lemma or definition like

def leftUnitor
    {C : Type u₁} [Category.{v₁} C]
    {D : Type u₂} [Category.{v₂} D]
    (F : C ⥤ D) :
    𝟭 C ⋙ F ≅ F :=
  _

from

def leftUnitor {C D : Cat.{v, u}} (F : C ⟶ D) :
    𝟙 C ≫ F ≅ F :=
  _

I'm not sure we can have such a tool.

[Sophie Morel]

We saw a great demonstration of an autogeneralizing tool today during Tim Gowers's talk, but it was only generalizing variables. I don't know if it could theoretically generalize universe levels.
More realistically, I'll have a look at the code Robin posted when I'm not in a crowded train.

[Joël Riou]

Robin Carlier said:

That being said, I had a go at simply copy-pasting the code in BicategoricalCoherence, replacing every instance of a 1-cell by a functor, and it "just works", you can play with it here.

Is there a way make a tactic which, given a goal like F₁ ⋙ (F₂ ⋙ F₃) ⋙ F₄ ⋙ 𝟭 _ ≅ F₁ ⋙ 𝟭 _ ⋙ F₂ ⋙ F₃ ⋙ F₄ would produce the dsimped expansion of this ⊗𝟭? (which is isoWhiskerLeft F₁ (F₂.associator F₃ (F₄ ⋙ 𝟭 C₅)) ≪≫ (Iso.refl (F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄ ⋙ 𝟭 C₅) ≪≫ isoWhiskerLeft F₁ (isoWhiskerLeft F₂ (isoWhiskerLeft F₃ F₄.rightUnitor))) ≪≫ isoWhiskerLeft F₁ (F₂ ⋙ F₃ ⋙ F₄).leftUnitor.symm)
Even though there is an unnecessary Iso.refl _ in this particular case, it seems that this is what would have been helpful for @Sophie Morel.

For reasons related to #mathlib4 > Functor identity `𝟭 _ ⋙ F = F` is definitional equality @ 💬, I do not think that a bare ⊗𝟭 should appear in polished code (and there is the general argument that we should not construct data using tactics), but using some related metacode as I suggest above could be helpful when constructing terms.

[Robin Carlier]

I can look at feasability of something like this, but I have a few things on my plate already so don’t expect it super soon.

What I have in mind would be an elaborator: you write something like ⊗𝟭, but it elaborates as "the right morphism in this context", and so you can freely use it in constructions because at the end it’s "just a macro" an the terms constructed are tactic-free. Then, ⊗≫ would be a macro for ≫ ⊗𝟭.hom ≫.

This is bound to be "more complicated" than the typeclass inference method, because the way I can see it working would involve looking at the expected types of the LHS/RHS of the ⊗𝟭, check they’re indeed "the same up to coherences" by matching at the Expr level, and then build inductively the morphism.

I’ll admit that I’m still a beginner at metaprogramming, so not sure if I can come up with something nice, but I can try and that could be a fun project.

[Joël Riou]

Actually, I am not sure it is necessary to do this! If we use ⊗𝟭 to create an isomorphism and we want to prove for example that it is compatible with shifts, we may just do dsimp which will expand ⊗𝟭 as a combination of associators, unitors, compositions, whiskering, and then infer_instance should work...

[Yuma Mizuno]

I think it would be useful to have metacode that generates more optimized expressions than the current ones, in the sense that they do not contain Iso.refls.

[Yuma Mizuno]

At the same time, I personally think that coherence isomorphisms (associators, ...) are "irrelevant", and I'm therefore willing to generate them by a tactic.

[Yuma Mizuno]

I wrote the assoc% term elaborator, which inserts appropriate associators: #26920. Manual inserting is not as easy as it might seem (as it can pass type checking even if it is not correct), so I believe assoc% is useful.

import Mathlib.Tactic.CategoryTheory.Associators

namespace CategoryTheory

open CategoryTheory

universe v₁ v₂ v₃ v₄ v₅ u₁ u₂ u₃ u₄ u₅
variable {A : Type u₁} [Category.{v₁} A]
variable {B : Type u₂} [Category.{v₂} B]
variable {C : Type u₃} [Category.{v₃} C]
variable {D : Type u₄} [Category.{v₄} D]
variable {E : Type u₅} [Category.{v₅} E]

variable (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) (I : D ⥤ E)

open Functor

local infixr:81 " ◁ " => Functor.whiskerLeft
local infixl:81 " ▷ " => Functor.whiskerRight
local notation "α_" => Functor.associator
local notation "λ_" => Functor.leftUnitor
local notation "ρ_" => Functor.rightUnitor

/-
Try this: (α_ F G H).hom
-/
example : (F ⋙ G) ⋙ H ⟶ F ⋙ (G ⋙ H) :=
  assoc%

/-
Try this: (α_ F G H).inv
-/
example : F ⋙ (G ⋙ H) ⟶ (F ⋙ G) ⋙ H :=
  assoc%

/-
Try this: F ◁ (α_ G H I).hom ≫ (α_ F G (H ⋙ I)).inv
-/
example : F ⋙ (G ⋙ H) ⋙ I ⟶ (F ⋙ G) ⋙ H ⋙ I :=
  assoc%

[Yuma Mizuno]

I would be grateful for feedback from anyone who is interested.