THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the functor structure of
set.image2 in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.