{ x : Kind } ⩓ { y : Kind }