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.