#
Homotopy Type Theory
dense relation > history (changes)

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

<dense relation

## 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

~~
~~
Last revised on June 14, 2022 at 16:26:17.
See the history of this page for a list of all contributions to it.