Table of Contents - 21.20.6.4. Direct image and inverse image
Definitions of the functionalized direct image and inverse image.
The functionalized direct (resp. inverse) image is the morphism component of
the covariant (resp. contravariant) powerset endofunctor of the category of
sets and relations (and, up to restriction, of its subcategory of sets and
functions). Its object component is the powerset operation defined in
df-pw.