Binary relations

Given two types and , a binary relation between and can be described as a function that, when given two witnesses and produces a which is inhabited iff and are related.