[[!redirects binary relation]] ## Definition ## A __binary relation__ over a type $A$ is a [[predicate]] $R$ over the product type $A \times A$ A __relation__ over a [[type family]] $A$ indexed by a type $I$ is a predicate $R$ over the [[dependent product]] type $$\prod_{i:I} A(i)$$ ## See also ## * [[dense relation]] * [[apartness relation]] * [[predicate]] * [[proposition]] * [[type family]]