(There have been many questions on MathOverflow about the axiom scheme of replacement, including a few with a similar flavour to mine. Some have very informative answers and link to excellent papers and blog posts. I've spent a while reading the older questions etc., and as far as I know, my question isn't answered in any of them — but it's entirely possible that it is and I missed it. In that case, I'll be grateful if someone points out where.)


Consider the following statement about sets and functions, which I'll call "axiom A":



> 
> **A.** For all well-ordered sets $(B, \leq)$, there exist a set $X$ and a function $p: X \to B$ with the following property: 
> 
> 
> 
> > 
> > for all $b \in B$, the fibre $p^{-1}(b)$ is an infinite set of smallest cardinality greater than that of $p^{-1}(b')$ for each $b' < b$.
> > 
> > 
> > 
> 
> 
> 


In the traditional notation of set theory, if $(B, \leq)$ is an ordinal $\beta$, then $p^{-1}(\alpha) \cong \aleph\_\alpha$ for each $\alpha \in \beta$. So, $X$ is the disjoint union $\coprod\_{\alpha \in \beta} \aleph\_\alpha$ and $p: X \to \beta$ is the obvious projection.


My question is about ETCS (Lawvere's [Elementary Theory of the Category of Sets](https://ncatlab.org/nlab/show/ETCS)) together with axiom A. In what follows, I'm going to take ETCS as the background theory. Thus, when I say "*this* is weaker than *that*", I mean weaker in the presence of ETCS. 


On the one hand, A isn't a theorem of ETCS (unless, of course, ETCS is inconsistent). That's because ETCS+A proves the existence of $\aleph\_\omega$ but ETCS alone doesn't.


On the other, if I'm not mistaken, A is weaker than replacement. That's because ETCS+replacement is bi-interpretable with ZFC, and unless I'm misremembering, the fact that ETCS+A is a *finite* list of axioms (not involving axiom *schemes*) somehow implies that it can't be as strong as ZFC.


So, it seems that axiom A is a weaker form of replacement. My question:



> 
> To what fragment of replacement is axiom A equivalent (in the presence of the axioms of ETCS)?
> 
> 
> 


That question is a little vague, so let me focus it more:



> 
> What's the simplest statement you can think of that's true in ETCS+replacement (or equivalently ZFC) but not provable in ETCS+A?
> 
> 
> 


I don't mind whether the statement is purely set-theoretic or from another part of mathematics. 


**Added later** Incidentally, "axiom A" is equivalent (under ETCS) to the following simpler statement:



> 
> for every set $B$, there exists a map into $B$ whose fibres all have different cardinalities.
> 
> 
> 


Formally: for all sets $B$, there exist a set $X$ and a map $p: X \to B$ such that for all $b, b' \in B$, if $p^{-1}(b) \cong p^{-1}(b')$ then $b = b'$.



How much Replacement does this axiom provide?
Asaf points out that Axiom A is true in $V\_{\delta}$ if $\delta$ is a $\beth$ fixed point. Full replacement only holds if $\delta$ is worldly. So, in $V\_{\delta}$ models of these, replacement implies a proper class of $\beth$ fixed points (since all worldly cardinals are $\beth$ fixed point-sized limits of $\beth$ fixed points), but Axiom A is compatible with the statement that there are no $\beth$ fixed points. In fact, ZFC does proves that there's a proper class of $\beth$ fixed points, since for any ordinal $\alpha$ the limit of the sequence $\beta\_0 = \alpha; \beta\_{n+1} = \beth\_{\beta\_{n}}$ is a $\beth$ fixed point greater than $\alpha$.


