Binary relations

'utils require import

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 ! !

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
! !

Ambiance: Primary hue Primary saturation Low hue Low saturation High hue High saturation Min contrast Max contrast Luminosity