Homotopy Type Theory relation > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

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

See also

• dense relation

• apartness relation

• predicate

• proposition

• type family