## 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)$$ ## See also ## * [[directed graph]] * [[predicate]] * [[proposition]] * [[type family]]