0PAP Proposition 7.4.4. If ff is strict, then f#f^{\#} defines a functor add(𝒫(Z′))→add(𝒫f(Z))\operatorname{add}\nolimits({\mathcal{P}}(Z^{\prime}))\to\operatorname{add}\nolimits({\mathcal{P}}_{f}(Z)) commuting with coproducts.