The Powerset Monad I am struggling to prove commutativity of the diagrams for the powerset monad in Category $\mathbb{Set}$.


*

*To show that $\mu:\mathcal{P}^{2}\longrightarrow \mathcal{P}$ given by $\mu_{X}:\mathcal{P}^{2}(X)\longrightarrow\mathcal{P}(X)$, $\{A_{i}:i\in I\}\mapsto\bigcup_{i\in I}A_{i}$
is a natural transformation, I must show that the diagram


$$
\newcommand{\ra}[1]{\!\!\!\!\!\!\!\!\!\!\!\!\xrightarrow{\quad#1\quad}\!\!\!\!\!\!\!\!}
\newcommand{\da}[1]{\left\downarrow{\scriptstyle#1}\vphantom{\displaystyle\int_0^1}\right.}
%
\begin{array}{llll}
\mathcal{P}^{2}(X) & \ra{\mu_{X}} & \mathcal{P}(X)  \\
\da{\mathcal{P}^{2}(f)} & & \da{\mathcal{P}(f)} \\
\mathcal{P}^{2}(Y) & \ra{\mu_{Y}} & \mathcal{P}(Y) \\
\end{array}
$$
commutes, where $f:X\longrightarrow Y$ and $\mathcal{P}(f)$ is given by $A\mapsto f(A)$.
I can show that $$\mathcal{P}(f)(\mu_{X}(\{A_{i}:i\in I\}))=\mathcal{P}(f)\big(\bigcup_{i\in I}A_{i}\big)=\bigcup_{i\in I}f(A_{i})$$ 
How do I show that $$\mu_{Y}(\mathcal{P}^{2}(f)(\{A_{i}:i\in I\}))=\mathcal{P}(f)(\mu_{X}(\{A_{i}:i\in I\}))=\bigcup_{i\in I}f(A_{i})$$ Is there any trick on how to use $\mathcal{P}^{2}(f)$?


*Also for the diagram


$$
\newcommand{\ra}[1]{\!\!\!\!\!\!\!\!\!\!\!\!\xrightarrow{\quad#1\quad}\!\!\!\!\!\!\!\!}
\newcommand{\da}[1]{\left\downarrow{\scriptstyle#1}\vphantom{\displaystyle\int_0^1}\right.}
%
\begin{array}{llll}
\mathcal{P}^{3}(X) & \ra{\mu_{\mathcal{P}(X)}} & \mathcal{P}^{2}(X)  \\
\da{\mathcal{P}\mu_{X}} & & \da{\mu_{X}} \\
\mathcal{P}^{2}(X) & \ra{\mu_{X}} & \mathcal{P}(X) \\
\end{array}
$$
Is it always true that $\mathcal{P}\mu=\mu \mathcal{P}$? Or there is another simpler way of showing that $$\mu_{X}\circ\mathcal{P}\mu_{X}=\mu_{X}\circ\mu_{\mathcal{P}(X)}$$
I'd appreciate any form of help. Thank you
 A: Note that, in general, we have
\begin{align}
\mathcal P(f)(x')&=\{f(x):x\in x'\}&
&x'\in\mathcal P(X)\\
\mu_X(x'')&=\bigcup x''\\&=\bigcup_{x'\in x''}x'\\
&=\{x:\exists x'(x\in x'\in x'')\}&
&x''\in\mathcal P^2(X)
\end{align}
hence, in particular,
\begin{align}
\mathcal P^2(f)(x'')
&=\mathcal P(\mathcal P(f))(x'')\\
&=\{\mathcal P(f)(x'):x'\in x''\}\\
\end{align}
For the fist question, note that
$$P^2(f)(\{A_i:i\in I\})=\{\mathcal P(f)(A_i):i\in I\}$$
hence the commutativity of the first diagram is equivalent to
$$\bigcup_{i\in I}\mathcal P(f)(A_i)=\mathcal P(f)\left(\bigcup_{i\in I}A_i\right)$$
which is true because both sides equals
$$\{f(a):\exists i\in I(a\in A_i)\}$$
For the second question, let $x'''\in\mathcal P^3(X)$.
Then
\begin{align}
(\mu_X\circ\mathcal P\mu_X)(x''')
&=\mu_X(\{\mu_X(x''):x''\in x'''\})\\
&=\bigcup_{x''\in x'''}\mu_X(x'')\\
&=\bigcup_{x''\in x'''}\bigcup_{x'\in x''}x'\\
&=\{x:\exists x'\exists x''(x\in x'\in x''\in x''')\}\\
\end{align}
on the other hand
\begin{align}
(\mu_X\circ\mu_X\mathcal P)(x''')
&=\mu_X\left(\bigcup x'''\right)\\
&=\bigcup\bigcup x'''\\
&=\bigcup\bigcup_{x''\in x'''}x''\\
&=\bigcup\{x':\exists x''(x'\in x''\in x''')\}\\
&=\{x:\exists x'\exists x''(x\in x'\in x''\in x''')\}\\
\end{align}
A: In this answer $\cup$ is an operator on sets that sends every set to the union of its elements: $$A\mapsto\cup A:=\bigcup_{a\in A}a$$
Actually $\mu_X$ can be recognized as this operation restricted to $\wp^2(X)$.

1)
For $\mathcal A\in\wp^2(X)$ or equivalently $\mathcal A\subseteq\wp(X)$ we have:$$\mathcal A\stackrel{\mu_X}{\mapsto}\cup\mathcal A\stackrel{\wp(f)}{\mapsto}f(\cup\mathcal A)$$(as you already noted) and:$$\mathcal A\stackrel{\wp^2(f)}{\mapsto}\{f(A)\mid A\in\mathcal A\}\stackrel{\mu_X}{\mapsto}\cup\{f(A)\mid A\in\mathcal A\}$$
So in order to prove the commutativity it is enough to show that: $$f(\cup\mathcal A)=\cup\{f(A)\mid A\in\mathcal A\}=\bigcup_{A\in\mathcal A}f(A)$$
The obvious equivalence of the following statements show that:


*

*$x\in f(\cup\mathcal A)$

*$\exists y\in\cup\mathcal A\;[x=f(y)]$

*$\exists A\in\mathcal A[\exists y\in A[x=f(y)]]$

*$\exists A\in\mathcal A[x\in f(A)]]$

*$x\in\bigcup_{A\in\mathcal A}f(A)$

2)
Let $\mathcal A_i\in\wp^2(X)$ or equivalently $\mathcal A_i\subseteq\wp(X)$ for every $i\in I$.
Then we have:
$$\{\mathcal A_i\mid i\in I\}\stackrel{\wp(\mu_X)}{\mapsto}\{\cup\mathcal A_i\mid i\in I\}\stackrel{\mu_X}{\mapsto}\cup\{\cup\mathcal A_i\mid i\in I\}$$and:
$$\{\mathcal A_i\mid i\in I\}\stackrel{\mu_{\wp(X)}}{\mapsto}\cup\{\mathcal A_i\mid i\in I\}\stackrel{\mu_X}{\mapsto}\cup(\cup\{\mathcal A_i\mid i\in I\})$$
Here the following statements are equivalent:


*

*$x\in\cup(\cup\{\mathcal A_i\mid i\in I\})$

*$\exists y\;[x\in y\in\cup\{\mathcal A_i\mid i\in I\}]$

*$\exists y\exists i\in I\; [x\in y\wedge y\in\mathcal A_i]$

*$\exists y[x\in y\wedge\exists i\in I\;[y\in\mathcal A_i]$

*$\exists y[x\in y\in\cup\mathcal A_i]$

*$x\in\cup\{\cup\mathcal A_i\mid i\in I\}$
This proves the commutativity of the diagram.
