Homotopy Type Theory relation > history (Rev #3)

Definition

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

See also

• directed graph

• predicate

• proposition

• type family