section funcomp variables {X Y Z:Type} def comp (f:X → Y) (g:Y → Z) :X → Z := λ x:X, g (f x) end funcomp #check comp infix `;` := comp constants A B C D:Type constants (f:A → B) (g:B → C) (h:C → D) #check comp #check comp f g #check f;g;h #check f ; @id B