The category of types with binary relations as morphisms.
A type synonym for Type, which carries the category instance for which morphisms are binary relations.