composition of functor in reverse order?

Stream: mathlib4

[Edison Xie]

import Mathlib

example (α β γ: Type*) (f : α → β) (g : β → γ) (x : α ): (g ∘ f) x = g (f x) := rfl

open CategoryTheory in
example {C1 C2 C3 : Type*} [Category C1] [Category C2] [Category C3]
    (F : C1 ⥤ C2) (G : C2 ⥤ C3) (X : C1) :
  (F ⋙ G).obj X = G.obj (F.obj X) := rfl

Why is the composition of functors in the reverse order of composition of functions? Is there any special reason or is this just the convention?

[Yaël Dillies]

This is generally the convention in category theory, yes. Same for eg morphisms

[Edison Xie]

Yaël Dillies said:

This is generally the convention in category theory, yes. Same for eg morphisms

then maybe imperial lecture notes need fixing :rolling_on_the_floor_laughing:

[Joël Riou]

This convention is not universally followed at all in the mathematical literature!

[Yaël Dillies]

Sorry, I meant the CategoryTheory convention :stuck_out_tongue_closed_eyes: