Add a primitive total one place fuction symbol $\tau$, to the language of set theory. Add the following axioms:

Extensionality: $\forall z \, (z \in x \iff z\in y) \implies x=y$

Sets with the same elements, are equal.

Define: $\alpha \text { is a type } \iff \exists x: \alpha=\tau(x) $

We will restrict Greek letters for types.

Types: $ {\sf Transitive \! : } \ \alpha < \beta < \gamma \implies \alpha < \gamma \\ {\sf Connected\!: } \ \alpha \neq \beta \iff \alpha < \beta \lor \beta < \alpha \\ {\sf well \ founded\!: } \ \phi(\alpha) \implies \exists \beta: \phi(\beta) \land \\\forall \alpha (\phi(\alpha) \implies \alpha \not < \beta) \\ {\sf Increament\!: }\ \forall \alpha \, \exists \beta: \alpha < \beta \\ {\sf Infinity\!: } \ \exists \lambda \neq 0: \forall \alpha < \lambda \, \exists \beta: \alpha < \beta < \lambda$

Typing: $ \forall y \in x\, (\tau(y) < \tau(k)) \iff \tau(x) \leq \tau(k)$

The type of a set is the limit to the type of its elements.

Predicative typed comprehension: $$ \forall \alpha \forall x_1,..,\forall x_n: \\ (\underset {i=1} {\overset {n} \bigwedge}\tau(x_i) < \alpha) \land \lim \tau ``\phi^\alpha =\alpha \\\implies \exists x \ \forall y \ (y \in x \iff \phi^\alpha)$$; where $\phi^\alpha$ is a formula having all of its quantifiers of the forms $$\forall k \, (\tau(k) < \alpha \implies); \\\exists k (\tau(k) < \alpha \, \land ..)$$, and its free variables are $y,x_1,..,x_n$, and $$\lim \tau``\phi =\alpha \iff \\\forall \zeta (\forall y (\phi \implies \tau(y) < \zeta) \iff \alpha \leq \zeta)$$

In English: for a type $\alpha$ if the limit to the type of all objects that a formula $\phi$ holds of is $\alpha$, and if the type of all variables (bound and free) in $\phi$ is strictly lower than $\alpha$, then $\phi$ defines a set.

Countability: Every set is countable.

Choice: Every set is well orderable.

Can this theory interpret $\sf PA$?

If we allow some impredicativity by replacing $\leq$ instead of $<$ in the quantifier and the free variable restrictions of the comprehension schema, and remove the countability axiom; would that increase the consistency strength to at least $ \sf Z_2$?