f : {A B C : Set} @$\rightarrow$@ ((A @$\rightarrow$@ B) @$\times$@ (B @$\rightarrow$@ C)) @$\rightarrow$@ (A @$\rightarrow$@ C)
f = \p x @$\rightarrow$@ (snd p) ((fst p) x)