Zulip Chat Archive

Stream: maths

Topic: equality between natural transformations


view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 06 2019 at 18:38):

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

view this post on Zulip Johan Commelin (May 06 2019 at 18:39):

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

view this post on Zulip 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. :-)

view this post on Zulip Johan Commelin (May 06 2019 at 19:36):

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

view this post on Zulip Kevin Buzzard (May 06 2019 at 19:44):

Better?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 06 2019 at 19:48):

/me :bulb:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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