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