I'm reading the paper Wellfounded trees in categories by Moerdijk and Palmgren. I'm having trouble understanding the proof of Theorem 7.2 (page 216), i.e. that in $\mathbf{ML}_{< \omega} \mathbf{W}$ the category $\mathbf{Sets}$ has W-types. The reason is that, even though they write that it is well-known that in $\mathbf{ML}_0$ the category $\mathbf{Sets}$ is locally Cartesian closed, I'm not sure I understand what dependent products actually look like.
For instance, they define $\sigma\colon PW \to W$ by $$ \sigma((a, f)) = (\mathsf{sup}(a, \pi_1 \circ f), p), $$ where $p$ is the appropriate proof-term, obtained from the assumption that $f$ is extensional. Since I expect $\sigma$ to be a function $\sigma\colon (\Sigma a \in \overline{A})\, \overline{W^{B_a}} \to \overline{W}$ preserving the equivalence relation, I should have that $a \in \overline{A}$ and $f \in \overline{W^{B_a}}$. But in order for $f$ to be extensional as required, we must have that $f$ is actually not just a function, i.e. a term of $\overline{W}^\overline{B_a}$, but a pair $(f', q)$ where $f' \in \overline{W}^\overline{B_a}$ and $q$ is a proof-term witnessing that $f'$ is extensional. But then $\pi_1 \circ f$ doesn't make sense! So, if I tried to reformulate the definition, I'd say $$ \sigma((a, (f', q))) = (\mathsf{sup}(a, \pi_1 \circ f'), p). $$ The problem is that if I try to write the remainder of the proof in this way, I run into a problem when I have to define the unique morphism $r\colon W \to X$. They say that $r$ can be proved to be extensional by $W^0$-induction, but in my case I cannot even define $r$ without knowing that it will be extensional.
What am I doing wrong?
Thanks in advance to anyone willing to look at my problem.
