{ x : Type } ⩓ { y : Type }