natural composition

Stream: new members

[Nicolas Rolland]

mathematical composition of function is defined

@[inline] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=
  fun x => f (g x)

Is there a natural composition operator which goes the other way ?

[Sky Wilshaw]

Consider the notation |>: https://leanprover-community.github.io/mathlib4_docs/Init/Notation.html#%C2%ABterm_|%3E_%C2%BB (doesn't answer the question)

[Jireh Loreaux]

There is in category theory.