# Homotopy Type Theory directed graph > history (changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

## 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.