Leaving aside communal inertia ("why change a perfectly fine presentation?"), which is of course significant, I don't see the benefit of this proposed reaxiomatization.
It is much shorter than the usual presentation of ZF- by axioms of Extensionality, Empty, Set union, Power, Separation, Replacement, and Infinity.
Sure, but length isn't an inherent indicator of quality.
This exposition of ZF- is actually very simple
Is it? Someone new to the field would have substantially more difficulty using it, I suspect, than using the usual $\mathsf{ZF-}$ axioms. Simplicity of presentation and simplicity of use are two different things, and in most situations I think the latter is more important than the former.
it appears to be pretty much natural and reduces all those diversily looking axioms into just two simple principles "we reflect, then specify!", that's all
Again, I don't really buy this: why should "we reflect, then specify" be an accepted bit of set-theoretic intuition? Motivating reflection is nontrivial. By contrast, the $\mathsf{ZF-}$ axioms are graded: consider the various levels of "justifiability" of e.g. Pairing, Infinity, Replacement, and Powerset. Someone who doesn't find all of them intuitive will still (probably) find some of them intuitive, and so a larger portion of the theory is "immediately acceptable." I think this is very useful for the pragmatic side of things: to a strong set theory skeptic we can argue that the "inoffensive part" of $\mathsf{ZF-}$ is still strong enough to do what they need, while it's not clear how to whip up something similar for your approach.
There's also the more technical aspect: if you're interested in fragments of $\mathsf{ZF-}$ (which I personally am very much), a more modular approach is significantly easier to use.
To sum up, I think that while this is of course a neat result, as an axiomatization of $\mathsf{ZF-}$ it is inferior to the standard one(s) in terms of intuitive appeal and immediate usability - and I don't think that its advantages make up for that.
I think the answer is to the positive. I was just wondering if Replacement can follow from inaccessibility of types, which happens to be the case! A point that I didn't see clearly at the begining. This shows that naive conception about types with sets constructed thereof is a strong notion! Since it can easily interpret set theory.
The proof is actually almost straighforward.
Lemma: there is no maximal type:
$\not \exists t^{max}: \forall \text{type } t \, (t < t^{max})$
Proof: suppose there is a maximal type $t^{max}$. Define the fixed function $f(y)=t^{max}$. Now take any set $x$ such that $y \in x$ and we'll have every type $t \leq f(y)$; contradicting Inaccessibility.
The proof of Replacement: for any definable function $f$ (not using symbol $B$) for any set $A$, there exists a set $B$ that is a set image of $A$ under $f$.
Proof: Define the function $i$ from $A$ as $i(x)=\tau(f(x))$ for each $x \in A$, so $i$ is the restriction of the composition $\tau \circ f$ to $A$. Now assume that for every type $t$ there exists some $i(x)$ for an $x \in A$ such that $t \leq i(x)$; by then we'd violate Inaccessibility. So there must exist a type $t$ that is strictly higher than the type of every $f(x)$ when $x \in A$, use this type in Typed Comprehension, and construct the set image of $A$ under $f$.
The proofs of Power and Set Union are straighforward also, since simply we take a type $t > \tau(x)$ and simply we can construct $P(x)$ and $\bigcup(x)$ by substituting this type in Typed comprehension with the relevant formulas.
The proof of Infinity is easy also, take $t$ in Typed comprehension to be the first limit type, and we can easily construct the set of all naturals. We can easily prove that no natural can have an infinite type, since otherwhise the types of all naturals with infinite types would constitute a descending type chain! Thus violating the Well Ordering schema.
So all axioms of $\sf ZF \text{ - Reg.} $ are proved in this theory, so clearly this theory would interpret $\sf ZFC$.
Best Answer
Call this new axiom system $K$.
First, note we can augment the reflection scheme to
$$ \exists x (trans(x) \land set(x) \land (\phi \iff \phi^x))$$
By simply doing case analysis on whether $\phi$ or $\neg \phi$ is true and applying the reflection principle in either case.
Now recall the class comprehension scheme of MK, which consists of all the axioms $A_\phi$ of the form
$$\forall \vec{P}\exists M (\forall x (set(x) \land \phi(\vec{P}, x) \iff x \in M))$$
For any formula $\phi(\vec{P}, x)$ (where $M$ does not appear). I claim each $A_\phi$ is provable from $K$.
For consider some transitive set $t$ such that $A_\phi$ is absolute for $t$. We wish to prove $A_\phi^t$. This formula becomes
$$\forall \vec{P} \subseteq t \exists M \subseteq t (\forall x \in t (\phi^t(\vec{P}, x) \iff x \in M))$$
Take some $\vec{P} \subseteq t$. Then such an $M$ exists by the separation axiom scheme. So we have proved the class comprehension scheme.
With the class comprehension scheme in hand, we can prove the consistency of ZF - Reg in a straightforward way. This is because we can develop the model theory of class-sized models and prove $V \models ZF - Reg$. We can then prove the soundness theorem for class-sized models to conclude that $ZF - Reg$ is consistent.