[[!redirects binary endorelation]] ## Definition ## A __binary endorelation__ over a type $A$ is a [[predicate]] $\mapsto$ over the product type $A \times A$. The type $A$ with the binary relation $\mapsto$ is called a __directed graph__, the terms $a:A$ are called __nodes__ or __vertices__, and the dependent types $a \to b$ are called __edges__. ## See also ## * [[relation]]