Name for `fun f => pure ∘ f`

Stream: Is there code for X?

[Markus Schmaus]

The function fun f => pure ∘ f, which appears in docs#map_eq_bind_pure_comp , is pretty basic, but I would like to give it a name. Is this function already defined somewhere? Does it have a common name?

[Mario Carneiro]

comp pure

[Markus Schmaus]

That's another way to construct that function, and given how short that is, maybe nobody has ever seen the need to give it a name. But I wanted to ask, just to make sure.

[Mario Carneiro]

I don't think I've seen it show up in practice very much

[Kyle Miller]

That function defines what one of the functors for the Kleisli adjunction does to morphisms. I'm not sure that has a name, and I couldn't find a name for it in mathlib or Lean.

The composition for the Kleisli category is defined in core Lean as docs#Bind.kleisliLeft, with notation <=< (one of the "fish" operators)