bicompr for linear maps

Stream: general

[Filippo A. E. Nuccio]

The definition of bicompr I find is

def bicompr (f : γ → δ) (g : α → β → γ) (a b) :=
f (g a b)

and it allows to compose an unary function f with a binary function g. I wonder if we have the same for more advanced morphisms, like

def foo (f : P →ₗ[R] Q) (g: M →ₗ[R] N →ₗ[R] P) : (M →ₗ[R] N →ₗ[R] Q) :=

for linear maps (or for other structures).

[Filippo A. E. Nuccio]

Oh yes, I found it: linear_map.compr₂.