How to prove relations between "classes" of types? After reading Effects as Sessions, Sessions as Effects, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System.

In a more generic fashion, how one can prove a relation (e.g. equivalence) between different "classes"* of types? Would that expressiveness test as done by Orchard and Yoshida be enough?

[*]: I don't know how to correctly define it, I don't want to use "kinds of types" or "types of types".
One approach to such questions is via encodings.  

Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding

$$
   \newcommand{\SEMBTYPE}[1]{\ulcorner #1 \urcorner}
   \newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack}
    \SEMB{\cdot} : L_1 \rightarrow L_2
$$

and then show that for all $L_1$ programs $M, N$ the following holds:

$$
   M \cong_1 N
   \qquad \text{iff} \qquad
   \SEMB{M_1} \cong_2 \SEMB{M_2}
$$

Here $\cong_i$ is a chosen notion of program equivalence for $L_i$. In order to do this for typed languages, one typically also maps $L_1$-types to $L_2$ by way of a function $\SEMBTYPE{\cdot}$ which is extended to typing environments, such that
something like the following holds:

$$
   \Gamma \vdash_1 M : \alpha
   \qquad \text{implies} \qquad
   \SEMBTYPE{\Gamma} \vdash_2 \SEMB{M} : \SEMBTYPE{\alpha}
$$
Here $\vdash_i$ is the typing judgement for $L_i$. 
The whole approach is called full abstraction.

In order to avoid the "curse of Church-Turing universality", one typically imposes conditions on $\SEMB{\cdot}$, e.g. that it's compositional, or closed under injective renaming. The more conditions $\SEMB{\cdot}$ meets, the stronger the full abstraction result.

This is also Orchard &amp; Yoshida are attempting to do (Theorems 1- 5), although they don't quite achieve it.