refactor(CategoryTheory/Monoidal): make ofTensorHom the default constructor
#7277
Conversation
…structor It seems all the users wish they had this constructor anyway, so lets just make it the default.
| @@ -41,6 +41,7 @@ instance (X : C) : MonoidalCategory (EndMonoidal X) where | |||
| tensorObj f g := f ≫ g | |||
| whiskerLeft {f g h} η := f ◁ η | |||
| whiskerRight {f g} η h := η ▷ h | |||
| tensorHom {X₁ Y₁ X₂ Y₂} f g := (f ▷ X₂) ≫ (Y₁ ◁ g) | |||
There was a problem hiding this comment.
I think this is the only place that actually benefitted from the old constructor, and obvious the benefit was pretty marginal!
There was a problem hiding this comment.
With the previous API, there was not even a chance to use the old constructor! I would suggest not merging this PR, as it goes in the other direction as @yuma-mizuno's planned refactor.
There was a problem hiding this comment.
I'm in no rush to get this in, so am happy for it to sit around until @yuma-mizuno gets back to their refactor. My impression though is that tensorHom is the operation we actually have available in (almost) all the concrete cases, and is therefore the more convenient constructor; and was that @yuma-mizuno's refactor is motivated by tensorHom being a bad simp-normal form, which is possibly orthogonal to whether it should be a constructor argument.
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
Closing, this has grown too many conflicts, and I no longer need it anyway. Hopefully at some point #6307 is revived and this becomes even more moot. |
It seems all the downstream call sites wish they had this constructor anyway, so lets just make it the default.
This partially reverts #6420 (Zulip discussion); the new data fields are good, but the defaults were backwards based on how the constructor is used.