#
Homotopy Type Theory
relation > history (changes)

Showing changes from revision #7 to #8:
Added | ~~Removed~~ | ~~Chan~~ged

~~
~~## Definition

~~
~~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)$

~~
~~A **binary relation** over types $A$ and $B$ is a predicate $\mapsto$ over the product type $A \times B$.

~~
~~## See also

~~
~~~~
~~
Last revised on June 15, 2022 at 22:36:24.
See the history of this page for a list of all contributions to it.