Homotopy Type Theory decidable directed graph > history (Rev #3, changes)

Definition

A decidable directed graph is a type $T$ with a function $(-) \to (-):T \times T \to \mathbb{2}$.

See also

• booleans
• decidable setoid
• decidable preordered type
• decidable strict order
• decidable dense strict order?