[proofplan]
Construct the factorization by sending each element of $Z$ to the same underlying element of $X$, equipped with the supplied proof that it satisfies $P$. Extensionality follows because equality in $S$ is inherited from equality in $X$. Uniqueness follows because any other factorization has the same image in $X$ after inclusion.
[/proofplan]
[step:Construct the factorizing map]
For each $z\in Z$, the hypothesis gives $P(g(z))$. Define
\begin{align*}
\bar g:Z\to S
\end{align*}
pointwise by
\begin{align*}
\bar g(z):=(g(z),P(g(z)))\in S.
\end{align*}
By definition of the inclusion, $i(\bar g(z))=g(z)$ for every $z$. Hence $i\circ\bar g=g$ as maps into $X$.
[/step]
[step:Prove extensionality of the factorizing map]
Suppose $z=_Z z'$. Since $g$ is extensional, $g(z)=_X g(z')$. Equality in $S$ is inherited from $X$, so the elements
\begin{align*}
\bar g(z)=(g(z),P(g(z)))
\end{align*}
and
\begin{align*}
\bar g(z')=(g(z'),P(g(z')))
\end{align*}
are equal in $S$. Thus $\bar g$ is extensional.
[/step]
[step:Prove uniqueness]
Let $h:Z\to S$ be another extensional map with $i\circ h=g$. For each $z\in Z$, the equations
\begin{align*}
(i\circ h)(z)=g(z)
\end{align*}
and
\begin{align*}
g(z)=i(\bar g(z))
\end{align*}
say that the underlying $X$-component of $h(z)$ is equal to the underlying $X$-component of $\bar g(z)$. Since equality in $S$ is inherited from $X$, this gives
\begin{align*}
h(z)=_S \bar g(z).
\end{align*}
Therefore $h=\bar g$ extensionally as maps from $Z$ to $S$.
[/step]
[step:Conclude the universal property]
The map $\bar g$ is extensional, satisfies $i\circ\bar g=g$, and is the only extensional map with that property. Thus the inclusion of the extensional predicate is a well-behaved subobject with the expected factorization property.
[/step]
[step:Summarize the factorization]
The proof forms the factorization by adding the predicate witness to each value of the original map. Inherited equality gives extensionality, and inclusion reflects equality because equality in the subset is defined by equality in the ambient set with equality.
[guided]
For every $z\in Z$, the hypothesis supplies a witness of $P(g(z))$. The factorizing map is therefore
\begin{align*}
\bar g(z)=(g(z),P(g(z))).
\end{align*}
This is an element of the subset $S$ with inherited equality, and applying the inclusion forgets only the predicate witness. Hence
\begin{align*}
i(\bar g(z))=g(z)
\end{align*}
for every $z$, so $i\circ\bar g=g$.
To check extensionality, assume $z=_Z z'$. Since $g$ is extensional, $g(z)=_X g(z')$. Equality in $S$ is inherited from $X$, so the two elements $(g(z),P(g(z)))$ and $(g(z'),P(g(z')))$ are equal in $S$. Thus $\bar g$ is an extensional map from $Z$ to $S$.
For uniqueness, let $h:Z\to S$ be extensional and satisfy $i\circ h=g$. For each $z$, the equality $(i\circ h)(z)=g(z)=i(\bar g(z))$ says that $h(z)$ and $\bar g(z)$ have the same underlying element of $X$. Since equality in the subobject is precisely inherited equality from $X$, we get $h(z)=_S\bar g(z)$ for every $z$. Therefore $h=\bar g$ extensionally.
[/guided]
[/step]
