Languages: Multi-sorted first order logic with equality $ =^s$ relations , and membership $\in^s$ relations, with sorts indexed by sequences on the naturals, with the following syntatical restrictions: $$ \in^s: s_n \longrightarrow s_{n+1} \\ =^s: s_n \longrightarrow s_n$$; meaning that $\in^s$ is a dyadic symbol from variables of sort $s_n$ on the left to variables of sort $s_{n+1}$ on the right; where $(s_n)_{n \in \mathbb N}$ is  decidable infinite monotonic strictly increasing sequence of naturals [at the metatheory].

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\]][1]? 

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