# Homotopy Type Theory relation > history (changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

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