 Then instance \(a\) being of type \(T\) in \(\mathbf{A}\) indicates that instance \(b\) is of type \(T'\) in \(\mathbf{C}\) if \(a\) and \(b\) are connected by a instance from \(\mathbf{C}\) and the relation \(f^{\wedge}(T) \Rightarrow g^{\wedge}(T')\) between the counterpart interpreted types is satisfied by all instances of \(\mathbf{C}\).