## Stream: maths

### Topic: equality between natural transformations

#### Floris van Doorn (May 06 2019 at 17:29):

@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 (May 06 2019 at 18:10):

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 (May 06 2019 at 18:37):

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 (May 06 2019 at 18:38):

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

#### Johan Commelin (May 06 2019 at 18:39):

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

#### Scott Morrison (May 06 2019 at 19:30):

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 (May 06 2019 at 19:36):

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

Better?

#### Johan Commelin (May 06 2019 at 19:48):

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.

/me :bulb:

#### Floris van Doorn (May 07 2019 at 00:50):

@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 (May 07 2019 at 02:02):

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 (May 07 2019 at 04:01):

@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...

Last updated: May 06 2021 at 18:20 UTC