Homotopy Type Theory dense relation > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

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

Revision on March 15, 2022 at 07:25:01 by Anonymous?. See the history of this page for a list of all contributions to it.