## Contents ## * table of contents {:toc} ## 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]] category: not redirected to nlab yet