init/function.lean in the core library has basic defintions and facts about functions between general types.
comp (function composition),
id (the identity function),
const (a constant function),
bijective. Note that many of these things live in the
function namespace, which has to be opened first.
variables (X Y Z : Type u)
variables (f : X → Y) (g : Y → Z) (h : Y → X)
example : bijective g → bijective f → bijective (g ∘ f) := bijective_comp
example : has_left_inverse f → injective f := injective_of_has_left_inverse
example : left_inverse h f → h ∘ f = id := id_of_left_inverse