Suppose $p\in\mathsf{Nm}$ and $f\colon [p]\rightarrow\omega_1$. Then there is some $\alpha<\omega_1$ so that $\bigcup f^{-1}[\{\alpha\}]$ contains a Namba tree.

For a tree $T\subseteq\omega_2^{<\omega}$ consider the game $\mathcal G^{\mathsf{Nm}}_T$: At most $\omega$-many rounds are played. In round $n$, player I plays some ordinal $\gamma_n<\omega_2$ and player II replies with some $t_n\in T$ properly extending the previously played $t_0,\dots,t_{n-1}$ so that the top ordinal of $t_n$ is $\geq\gamma_n$. Player I wins if player II has no valid moves, but loses in case II manages to survive through $\omega$-many rounds. Observe that $T$ contains a Namba subtree iff player II has a winning strategy in $\mathcal G^{\mathsf{Nm}}_T$. For the more difficult direction, note that if $\tau$ is a winning strategy for II then the tree of plays by II consistent with $\tau$ that come up in a run of the game is a Namba tree.

For $\alpha<\omega$, let $\mathcal G_\alpha$ be $\mathcal G^{\mathsf{Nm}}_{\bigcup f^{-1}[\{\alpha\}]}$. We are done if we can show that player II has a winning strategy in $\mathcal G_\alpha$ for some $\alpha<\omega_1$.

So suppose toward a contradiction that this is not the case. As all games $\mathcal G^{\mathsf{Nm}}_T$ are open, this means that player I has a winning strategy $\sigma_\alpha$ in each game $\mathcal G_\alpha$.

We will now take on the role of player II and play against all $\sigma_\alpha$ simultaneously. In round $n$, let $\Gamma_n$ be the supremum over all responses of $\sigma_\alpha$ to our moves so that we did not yet lose against $\sigma_\alpha$. We now properly extend our previously played $t_0,\dots, t_{n-1}$ to some $t_n\in p$ so that the top ordinal of $t_n$ is $\geq\Gamma_n$ which is possible as $p\in\mathsf{Nm}$ and $\Gamma_n<\omega_2$.

After $\omega$-many rounds, we have constructed a cofinal branch $b$ through $p$, namely the downwards closure of $$\{t_n\mid n<\omega\}.$$ But then for $\alpha=f(b)$, we have survived against $\sigma_\alpha$, contradiction!

Suppose $\mathrm{CH}$ holds. Then Namba forcing does not add reals.

Suppose $\dot x$ is a name for a real and $p\in\mathsf{Nm}$. We can build a fusion sequence $(p_n)_{n<\omega}$ blow $p$ so that for each $n$-splitting node $t$ of $p_n$, $p_n\upharpoonright t$ decides $\dot x_n$. Here, $p_n\upharpoonright t=\{s\in p_n\mid s\subseteq t \vee t\subseteq s\}$. Let $p_\omega$ be the fusion along this sequence.

We now define a function $f\colon [p_\omega]\rightarrow \mathbb R$ so that for every cofinal branch $b$ through $p_\omega$, $f(b)$ is the unique real $y$ which collects the decision of $p_\omega$ about $\dot x$ along $b$, i.e. $$\forall n<\omega\exists t\in b\ p_\omega\upharpoonright t\Vdash\dot x(\check n) = \check y(\check n).$$ By the technical lemma and $\mathrm{CH}$, there is some real $y$ so that $f^{-1}[\{y\}]$ contains some $q\in\mathsf{Nm}$. But now it is clear that if $G$ is $\mathsf{Nm}$-generic with $q\in G$ then $\dot x^G=y\in V$.

Suppose that $X\prec H_\theta$ is countable. Then the Chang tree for $X$ is $$\mathrm{Chang}_X=\{t\in\omega_2^{<\omega}\mid \exists X\sqsubseteq Y\prec H_\theta\ t\in Y\}.$$ We say that $X$ is a Namba model if $\mathrm{Chang}_X$ contains a Namba tree.

Let $\mathbb{P}$ be a forcing, $\theta$ sufficiently large and regular. If $X\prec H_\theta$ is countable with $\mathbb{P}\in X$ and if $p\in\mathbb{P}\cap X$, we say that $X$ is $(p,\mathbb{P})$-semiproper iff there is some $q\leq p$ with $$q\Vdash \check X\sqsubseteq \check X[\dot G].$$ We also say that $X$ is $\mathbb{P}$-semiproper if $X$ is $(p,\mathbb{P})$-semiproper for all $p\in \mathbb{P}\cap X$.

For sufficiently large regular $\theta$ and countable $X\prec H_\theta$, the following are equivalent:

$(1)$ $X$ is $\mathsf{Nm}$-semiproper.

$(2)$ $X$ is a Namba model.

$(1)\Rightarrow(2):$ Let $G$ be $\mathsf{Nm}$-generic so that $X\sqsubseteq X[G]$ and let $b$ be the generic branch through $\omega_2^{<\omega}$. Clearly, $\mathrm{ran}(\bigcup b)$ is cofinal in $\omega_2$, $b\in X[G]$ and $b\subseteq X[G]$. It is not difficult to see that for any $t\in b$, we must have that there is some $X\sqsubseteq Y\prec H_\theta^V$ with $t \in Y$ and $Y\in V$ (in $V[G]$, we may take $Y=X[G]\cap V$ and the existence of such $Y$ is absolute).

This shows that if $q\in G$ is such that $q\Vdash \check X\sqsubseteq\check X[\dot G]$ then $q\subseteq \mathrm{Chang}_X$, so $X$ is a Namba model.

$(2)\Rightarrow(1):$ Let $p_0\in X\cap \mathsf{Nm}$ and let $D_n$ enumerate the dense subsets of $\mathsf{Nm}$ in $X$. By gluing together trees, we can find a fusion sequence $p_{n}$ so that whenever $1\leq n$, $t\in p_n$ is a $n$-splitting node of $p_n$ then for all immediate successors $s$ of $t$ in $p_n$, the condition $$p_n\upharpoonright s=\{u\in p_n\mid u\subseteq s \vee s\subseteq u\}$$ is in $D_{n-1}$. In fact, we may assume $p_n\in X$ by elementarity. Hence the fusion $p_\omega=\bigcap_{n<\omega} p_n$ is a $\mathsf{Nm}$-condition.

Now let $q_\ast$ be the Chang reduction of $p_\omega$ along $X$. We will see that $q_\ast\Vdash\check X\sqsubseteq \check X[\dot G]$. Suppose that $\dot x\in X$ is a name for a countable ordinal and $r\leq q_\ast$ decides the value of $\dot x$. For some $n<\omega$, $D_n$ is the set of conditions deciding $\dot x$. So if $s$ is the immediate successor of a $n$-splitting node in $p_{n+1}$ and $s\in r$ then $p_{n+1}\upharpoonright s$ and $r$ must decide the same value $\alpha$ for $\dot x$ as they are compatible. Finally, as $s\in \mathrm{Chang}_X$, there is some $X\sqsubseteq Y\prec H_\theta$ with $s\in Y$ and hence $p_{n+1}\upharpoonright s\in Y$, so in fact $\alpha\in Y$. But $Y$ and $X$ have the same countable ordinals, so $\alpha\in X$.

Namba forcing is semiproper iff $\mathrm{SCC}_{\mathrm{cof}}$ holds.

Let $\theta$ be sufficiently large and regular. The set of Namba models is projective stationary in $[H_\theta]^\omega$. That is, for every club $\mathcal C\subseteq[H_\theta]^\omega$, the set $\{X\cap\omega_1\mid X\in\mathcal C\wedge X\text{ is a Namba model}\}$ contains a club.

Let $\mathcal C$ be a club in $[H_\theta]^\omega$ and let $S\subseteq \omega_1$ be stationary. We have to find a Namba model $X\in\mathcal C$ with $X\cap\omega_1\in S$. We may enrich $H_\theta$ with some structure, resulting in $\mathcal H$ so that any countable $X\prec \mathcal H$ is in $\mathcal C$. We will also assume that $\mathcal H$ admits definable Skolem terms, so we can take hulls.

Define $f\colon[\omega_2^{<\omega}]\rightarrow\omega_1$ via $f(b)=$ least $\alpha\in S$ so that $\mathrm{Hull}^{\mathcal H}(\alpha\cup b)\cap\omega_1=\alpha$. Note that such an $\alpha$ must exist as $S$ is stationary. By the technical lemma, there is some $\alpha\in S$ so that $f^{-1}[\{\alpha\}]$ contains some $q\in\mathsf{Nm}$. If we let $X=\mathrm{Hull}^{\mathcal H}(\alpha)$, this means that $q\subseteq \mathrm{Chang}_X$ and hence $X$ is a Namba model, $X\in\mathcal C$ and $X\cap\omega_1\in S$.

Namba forcing is statioary set preserving.

Let $S\subseteq\omega_1$ be stationary and $\dot C$ a $\mathsf{Nm}$-name for a club in $\omega_1$ and $p\in\mathsf{Nm}$. By the previous proposition, if $\theta$ is sufficienlty large and regular, there is some Namba model $X\prec H_\theta$ so that $\delta:=X\cap\omega_1\in S$ and $\dot C, p\in X$.

Hence $X$ is $\mathsf{Nm}$-semiproper. If $q\leq p$ is any condition so that $q\Vdash\check X\sqsubseteq \check X[\dot G]$ then it is easy to see that $q\Vdash\check\delta\in\dot C$.