f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C) f = \p x -> (snd p) ((fst p) x)