[[!redirects binary relation]] ## Definition ## 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)$$ A __binary relation__ over types $A$ and $B$ is a [[predicate]] $\mapsto$ over the product type $A \times B$. ## See also ## * [[directed graph]] * [[predicate]] * [[proposition]] * [[type family]] category: not redirected to nlab yet