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$ 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 writtin as items of $s$.

>Is this equivalent to Tangled Type Theory "$\sf TTT$" of Holmes [see: [Holmes p:11][1], [Holmes p:4-5][2]]? 

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?!


  [1]: https://arxiv.org/pdf/1503.01406.pdf
  [2]: https://randall-holmes.github.io/Papers/tangled.pdf