  We can then define in type theory when two such sets \(A, a, R\) and \(B, b, S\) are equal: this is the case iff there is a bisimulation \(T\) between \(A\) and \(B\) such that \(Tab\) holds. A bisimulation is a relation