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.

To clarify variables are indexed by naturals but the relations $\in,=$ to be indexed by sequences of naturals as qualified above.

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