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

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

Definition

A binary ~~relation~~ endorelation $R \mapsto$ R \mapsto over a type $A$ is dense if it comes with a family of dependent terms

a : A, b : A ⊢ d (a, b) : R (a, \mapsto b) \to ‖ \sum_{c : A} R (a, \mapsto c) \times R (c, \mapsto b) ‖

a:A, b:A \vdash d(a, b): ~~R(a,~~ (a \mapsto b) \to \Vert \sum_{c:A} ~~R(a,~~ (a \mapsto c) \times ~~R(c,~~ (c \mapsto b) \Vert

See also

Revision on March 17, 2022 at 20:53:22 by Anonymous?. See the history of this page for a list of all contributions to it.