Functor identity `𝟭 _ ⋙ F = F` is definitional equality

Stream: mathlib4

[Yuma Mizuno]

Robin Carlier said:

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!

Side remark: this was not the case for Lean 3, but we now have more definitionally equalities.

[Robin Carlier]

Oh I don’t remember this fact about lean 3, that’s interesting. I have sometimes wondered if things wouldn’t in fact be better if functor composition was not defeq-associative and defeq-unitary (but still prop-eq associative and prop-eq unitary).

[Yuma Mizuno]

Actually, it is very easy to write "type incorrect" expressions, some of them may be found in e.g., docs#CategoryTheory.Adjunction file.

[Robin Carlier]

Yes, I remember fixing one in whiskering as well, and that what made me think that It’d be better if lean was throwing an error in cases like this, which it would if things were not defeq.

[Joël Riou]

I just would like to say that replacing Functor.associator _ _ _, etc, by Iso.refl _ would be problematic. When we want to show certain properties of natural isomorphisms, for example show that an isomorphism is compatible with shifts (which are recorded in instances Functor.CommShift: this applies in particular for triangulated functors), the source and the target of an associator are not equipped with definitionally equal instances of Functor.CommShift(but they are compatible, see https://github.com/leanprover-community/mathlib4/blob/7deb334c5f5104f4edad1a6396dd02a8cddefb86/Mathlib/CategoryTheory/Shift/CommShift.lean#L343-L347 ). In #20490, with @Sophie Morel, we changed the definition of the composition of adjunctions by adding explicit associators, and this way we got better automation (for things like adjunctions between triangulated categories, see #20337).

[Robin Carlier]

@Joël Riou , I agree with you, which is why I said "even worse" in my message, and said it’s "a bug".
I don’t advocate for this and I’ve also had cases of very slow elaboration or bad automation when trying to power through by defeq abuse.
(Though, I wonder how much we can get away with Iso.refl _ if we provide the right type hints? Is it really different to write Functor.associator _ _ _ and (Iso.refl _ : (_ ⋙ _) ⋙ _ ≅ _ ⋙ _ ⋙ _)?) (Edit: your example about CommShift shows that we probably can’ t do that everywhere, at the very least).

But I’m also worried that the fact that this is a possibility makes it much harder to write a suitable "Categorical composition": when writing ⊗≫, there’s always the possibility that the LHS or RHS unifies with the "wrong" thing due to that defeq, right?

[Notification Bot]

6 messages were moved here from #mathlib4 > can bicategory infrastructure be applied to Cat? by Yuma Mizuno.

[Sophie Morel]

I tried to be very careful about not abusing defeq in the project that Emily mentioned, but it was not always easy for the reason that Robin was talking about: sometimes I would put a unitor or associator in the wrong direction, and it would still be accepted! In the end I had to make a lot of variable explicit, which helped with speed issues too. But it was painful, and the biggest problem is that it makes the code more painful to fix if I make a change somewhere upstream.

[Yuma Mizuno]

Can we set a transparency setting somewhere so that Lean cannot see these defeqs?

[Sophie Morel]

I don't know what a transparency setting is, but I would love a way to force Lean to be more annoying. (Just on this particular point though.)

[Yuma Mizuno]

Here the transparency setting means putting irreducible at some definitions, but this is just a naive idea.

[Sophie Morel]

Thanks for the explanation!

[Robin Carlier]

I tried blindly slapping an irreducible on Functor.comp, it doesn’t work super well, and we have to put an unseal Functor.comp in each time we want to define a natural transformation to/from a composition of functors.

[Yuma Mizuno]

Putting irreducible only to comp.map is enough to hide the undesired defeqs, which is a much milder setting than putting irreducible to the entire Functor.comp.

@[irreducible]
def compMap (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
   G.obj (F.obj X) ⟶ G.obj (F.obj Y) :=
  G.map (F.map f)

@[simps obj]
def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
  obj X := G.obj (F.obj X)
  map f := compMap F G f

[Yuma Mizuno]

By applying this change to downstream files, Lean found that the statement of docs#CategoryTheory.isoWhiskerRight_left, which is

    isoWhiskerRight (isoWhiskerLeft F α) K =
    Functor.associator _ _ _ ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫
      (Functor.associator _ _ _)

is type incorrect. The correct statement is

    isoWhiskerRight (isoWhiskerLeft F α) K =
    Functor.associator _ _ _ ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫
      (Functor.associator _ _ _).symm

[Yuma Mizuno]

WIP branch for this experiment: #26601. Anyone interested is welcome to ask about write access permissions.

[Sophie Morel]

Nice! It's very easy to make this kind of mistake, I had a Functor.leftUnitor instead of Functor.rightUnitor in some of my code and it was typechecking, I only noticed when I was trying to prove further properties. (Not because of an error in Lean, but because I wrote things out on paper and saw that the identity functor was on the wrong side.)

[Sophie Morel]

Looking at the error message for your branch, I notice a lot of errors in Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean, which reminds me that I had some beef with the way full subcategories are implemented in mathlib and was toying with the idea of suggesting a refactor.

[Robin Carlier]

Whoops, isoWhiskerRight_left is my doing...

[Robin Carlier]

(Regarding full subcategories, there is #26446 in the brewing, which I’m hyped for)

[Sophie Morel]

Robin Carlier said:

(Regarding full subcategories, there is #26446 in the brewing, which I’m hyped for)

Yes, that's exactly what I wanted to do!

[Sophie Morel]

Okay, now I need to leave reviews so that it gets merged.

[Robin Carlier]

It’s still tagged "WIP" though.

[Yuma Mizuno]

I continued to further downstream files.

One thing I found is that to prove

def equivalence₂CounitIso :
    (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ⋙ F ⋙ eB.inverse ≅ 𝟭 B :=
  sorry

where e, eA, and eB are equivalences, in the AlgebraicTopology\DoldKan\Compatibility.lean file, we now have to give an isomorphism of the form

(A ⋙ B ⋙ C) ⋙ D ⋙ E ≅
  A ⋙ ((B ⋙ C) ⋙ D) ⋙ E

at the first step of the proof. Of course we can write it, but I feel I now really want to the machinery what we have in the bicategory library (constructing this by a tactic or an instance resolution).

[Robin Carlier]

I wonder how much it is possible to have machinery not only for functors and natural transformations but also for other "unbundled bicategory-like" ("meta-bicategories"?) structures? In a recent series of PR I play with "categorical transforms of cospans", in #26447 I show that whatever this gadget is, it behaves like a bicategory (the reason it’s not one is, as usual, universes...), but I don’t have any tooling so the proof that when constructing equivalences, the right triangle identity is implied by the left triangle identity ends up looking like this while it’s in fact exactly the one in the Bicategory setting

[Robin Carlier]

(note that in the situation above, at least aesop_cat finds that the meta-bicategory is strict so replaces "by bicategory" but you still have to painfully write the coherence 2-cells by yourself...)

[Robin Carlier]

(Though, I can golf this particular proof to a non-calc one so the point don’t really apply in this case, but I think there might be other situations where this would be nice).

[Yuma Mizuno]

It would be nice to have machinery that can be applied to any "bicategory-like" situations, not only Category/Functor/NatTrans.

[Yuma Mizuno]

Would it work to annotate associators like morphisms and write a tactic that try to apply them to goals? (It seems to be a non-Prop simp?)

[Yuma Mizuno]

I made several fixes on this direction, but there are too many files to be touched, and I'm not sure I can continue to work on this right now.

As a tentative achievement, I made a PR #26701, which fixed some associator directions and inserted associators and unitros in several files.