There seems to be a reasonable category-theoretic question here, about morphisms between well founded relations and the reflection into the full subcategory of reflective ones.

I am a categorist and I think Martin is or was an algebraist and therefore a user of category theory. So please can we forget the set-theoretic notation and jargon. I don't see what "obvious diagram" is meant in the question. It is not possible to get a categorical understanding of a topic by wrapping the existing symbolic notation (especially from set theory) in a few diagrams.

In 1974 at the top of the agenda in category theory was to show that elementary toposes could do everything that sets could do. In particular, several authors gave translations of higher order logic into the axioms for a topos.

Gerhard Osius was the one person who took $\in$-structures seriously and reconstructed Zermelo set theory within any elementary topos.

He did this by representing any binary relation $(X,\prec)$ as a **coalgebra** $\alpha:X\to{\mathcal P} X$ for the powerset functor, with
$$ \alpha(x) \;=\; \{y|y\prec x\} \quad\mbox{or}\quad y\prec x\iff y\in\alpha(x). $$
More significantly, he observed that the **subset** relation from set theory is a **coalgebra homomorphism**. Such homomorphisms are also characterised as **bisimulations** and in fact Dimity Mirimanoff had recognised in 1917 that subset inclusions are like this, calling them "isomorphismes".

It is easy to see that $(\prec)$ is extensional iff $\alpha$ is mono. Osius used recursion, in the form of a 3vs1 coalgebra-to-algebra homomorphism, instead of well-foundedness. The latter was implicit in his work and that of Christian Mikkelsen (who gave a categorical proof of the recursion theorem).

My work in the 1990s gave the definition of a well founded coalgebra for any endofunction of $\mathbf{Set}$ that preserves inverse images and proved the recursion theorem for them. In this decade I relaxed the condition on the functor to preserving monos and identified the properties that are required of the category to prove the recursion theorem.

That is enough background to formulate the original question properly: in the category of well founded coalgebras, does the inclusion of the full subcategory of extensional ones have a left adjoint?

The set-theoretic result is attributed to Andrzej Mostowski. It uses recursion and the axiom-scheme of replacement.

However, all that we need, at least for the basic situation, is a **quotient** of the carrier, which any ordinary mathematician would obtain using an **equivalence relation**, with no need for Replacement. This is what I did in my 1996 JSL paper.

The equivalence relation is defined by co-recursion, so we could take this step-by-step.
The successive quotients are obtained by **factorising** the structure map $\alpha$ as an surjective function followed by an injective one. We obtain the extensional reflection as the fixed point of this construction.

Now this suggests making serious use of categorical tools, in particular replacing "monos" with a **factorisation system**. This is what I have done in my recent paper *Well Founded Coalgebras and Recursion*.

The follow-up paper, called *Ordinals as Coalgebras* applies all of this theory with posets instead of sets and examines various notions of constructive ordinals.

Using the flexibility of category theory, the "Mostowski" extensional quotient and (some version of) the "ordinal rank" are examples of the same construction.

However, in the case of the "plump" ordinals, the iterated factorisation does not converge. $\omega\cdot 2$ does not exist in the simplest non-classical elementary topos.

Set theorists will tell me that I need the axiom-scheme of replacement to do it, but my intention is to turn that argument on its head. General transfinite iteration of functors can be expressed using the same categorical ideas as the extensional reflection. I propose this as the **replacement for replacement** in the **native language of category theory**, which is to say using **adjointness in foundations**, as Bill Lawvere taught us.

All of my own work mentioned above, together with full references for Osius and others, is on my website: http://www.paultaylor.eu/ordinals/