equality between natural transformations

Stream: maths

[Floris van Doorn]

@Johan Commelin @Reid Barton @Scott Morrison
In #986 the following issue came up: how do we formulate equalities between natural transformations? We can of course use α = β, but we can also use ∀X, α.app X = β.app X (of course, these are equivalent). I would have a preference for the latter: I think in general equalities between morphisms are easier to work with. In either case, we should choose one of the options, and then consistently stick with it throughout the library.

One disadvantage when we use α = β is that we sometimes have to insert unitors/associators between functors, which disappear on the morphism level. For example:

variables {C : Type u₁} [category.{v₁} C]
variables {D : Type u₂} [category.{v₂} D]
variables {G : D ⥤ C} {F : C ⥤ C}
example (α : F ⟶ functor.id C) (β : G ⋙ F ⟶ G) : whisker_left G α = β ≫ (right_unitor G).inv :=
sorry
example (α : F ⟶ functor.id C) (β : G ⋙ F ⟶ G) (X : D) : α.app (G.obj X) = β.app X :=
sorry

[Johan Commelin]

I'm not sure if I understand the reason lying behind your proposal... but I trust your experience. I can't say much about how well your suggestion would "compose". But presumably you are claiming it will be at least as good as our current setup...

[Floris van Doorn]

One of the questions is what would be more useful to tidy. Does tidy apply ext before simp when proving an equality between natural transformations? If so, a lemma like whisker_left G α = β ≫ (right_unitor G).inv will probably never be applied by tidy, while α.app (G.obj X) = β.app X would be.

But presumably you are claiming it will be at least as good as our current setup...

Probably there are (small) trade-offs either way.

[Johan Commelin]

I think ext appears before simp in the list of tactics...

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/00aaf05a00b928ea9ac09721d87ae5d2ca1ae5a1/src/tactic/tidy.lean#L42

[Scott Morrison]

In some recent work (on stalks) I actually switched it around. Tidy seems to work between with ext after simp, so I'd prefer we get used to that. :-)

[Johan Commelin]

I can't parse your last sentence... Could you rephrase?

[Kevin Buzzard]

Better?

[Johan Commelin]

Aah... @Scott Morrison You switched ext and simp around?
I should just go to bed. I thought you were saying you switched from \a = \b to the version that Floris is proposing.

[Johan Commelin]

/me :bulb:

[Floris van Doorn]

@Scott Morrison Interesting! How often do you have to insert unitors. Is that annoying?

About the unit-counit laws specifically: do we want to "abuse" that functor.id ⋙ F = F ⋙ functor.id definitionally, or do we want to use both unitors?

[Scott Morrison]

I guess I don't have an opinion about the functor.id ⋙ F = F ⋙ functor.id trick. If we get burnt by it, it's unlikely to be much trouble to fix.

[Johan Commelin]

@Floris van Doorn This commit https://github.com/leanprover-community/mathlib/pull/986/commits/56a95da8dbfd7610bc99cf72f621f8c967204604 by Scott shows why I'm inclined to go for the \a = \b version...