Category-theoretic applicative functors

Stream: mathlib4

[Vilim Lendvaj]

Hello everyone!
I've written instance (F : Type u → Type v) [Applicative F] [LawfulApplicative F] : (ofTypeFunctor F).LaxMonoidal and I'd like to make a PR to put it into Mathlib.
Where do I put it? CategoryTheory.Monoidal.Types.Basic? CategoryTheory.Monoidal.Types.Functor? CategoryTheory.Monoidal.Functor.Types?

[Vilim Lendvaj]

Well, for now I've made a PR: https://github.com/leanprover-community/mathlib4/pull/30407
It's my first contribution so please tell me everything I did wrong :man_bowing:

[Yaël Dillies]

Hint: You can type #30407 and Zulip will render it as #30407

[Vilim Lendvaj]

Thaw would be more work, since it's one click to select the entire URL bar, but two clicks to select a word to copy it.

[Vilim Lendvaj]

But I guess it takes up less space in the message
I'll do that in the future.