Binary relations 'utils require import Try It Out > Required module: utils Given two types A Type ’A -> A and B Type ’B -> B, a binary relation between A A and B B can be described as a function that, when given two witnesses a A ’a -> a and b B ’b -> b produces a Set0 Type which is inhabited iff a a and b b are related. 'Relation Type ? ? def ! ! Try It Out > Type 'A -> Relation ( A A ) 'r -> 'reflexive A 'a -> r ( a a ) ? def 'symmetric A 'x -> A 'y -> r ( x y ) 'rxy -> r ( y x ) ? ? ? def 'transitive A 'x -> A 'y -> A 'z -> r ( x y ) 'rxy -> r ( y z ) 'ryz -> r ( x z ) ? ? ? ? ? def ! ! Try It Out >