Homotopy Type Theory relation > history (Rev #1)

Definition

A binary relation over a type $A$ is a predicate $R$ over the product type $A \times A$

A relation over a type family $A$ indexed by a type $I$ is a predicate $R$ over the dependent product? type

\prod_{i:I} A(i)

See also

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