Add a notion oFunctor_compose that composes two oFunctors.
The name oFunctor_compose was already in use, for the composition lemma of oFunctor_map. I thus renamed {o,r,ur}Functor_{ne,id,compose,contractive} into {o,r,ur}Functor_map_{ne,id,compose,contractive}, which is also more consistent with the rest of the development (we had names like auth_map_compose, excl_map_compose, etc.).
This is a breaking change /cc @iris-users