Homotopy Type Theory directed graph > history (Rev #1)

Definition

A binary relation over a type $A$ is a predicate $\to$ over the product type $A \times A$. The type $A$ with the binary relation $\to$ 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

• dense relation

• apartness relation