Languages: Multi-sorted first order logic with equality and membership, where for each natural $n$ we have variables $x_i^n$ of sort $n$, and for each decidable monotonic strictly increasing sequence of naturals $s$ we have binary relation symbols $=^s, \in^s$ with the following syntatical restrictions: the symbol $\in^s$ can only occur between variables of sort $s_n$ on the left to variables of sort $s_{n+1}$ on the right, generally denoted as $x_i^{s(n)} \in^s x_j^{s(n+1)}$ [where $s(n)$ is the $n^{th}$ term in the sequence $s$]. On the other hand, the symbol $=^s$ can only occur between variables of the same sort, generally denoted as $x_i^{s(n)} = x_j^{s(n)}$.

Notation: for simplicity we'll only write the type of a variable at quantification.

Axioms:

Extensionality: $ \forall x^{s_{n+1}} \, \forall y^{s_{n+1}}: \forall z^{s_n} \, ( z \in^s x \iff z \in^s y ) \implies x=^sy$

Comprehension: $\exists x^{s_{n+1}} \forall y^{s_n} (y \in^s x \iff \phi^s(y))$;

where $\phi^s$ only uses $\in^s,=^s$ as predicates, and all variables raised to $s_n$ types.

Is this equivalent to Tangled Type Theory "$\sf TTT$" of Holmes [see Holmes p:11]?

In the presentation by Holmes there is seeminly one membership and equality relation, unlike here where there is one per type sequence. I was personally thinking of a proof by compactness since every finite fragment of $\sf TTT$ per sequence $s$ is interpretable here, but I'm not that sure?!