[[!redirects dense]] ## Definition ## A [[binary relation]] $R$ over a type $A$ is __dense__ if it comes with a family of dependent terms $$a:A, b:A \vdash d(a, b): R(a, b) \to \Vert \sum_{c:A} R(a, c) \times R(c, b) \Vert$$ ## See also ## * [[relation]] * [[dense strict order]]