Language: 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$ [with 0 in its domain] ,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}$ item in 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)} =^s x_j^{s(n)}$.
Notation: for simplicity we'll only write the type of a variable at quantification.
Axioms: [Multi-sorted ID axioms for each sequence $s$] +
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 the sorts of all variables written as items of $s$.
Is this equivalent to Tangled Type Theory "$\sf TTT$" of Holmes [see: Holmes p:11, Holmes p:4-5]?
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?!
