Homotopy Type Theory relation > history (changes)

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


A relation over a type family AA indexed by a type II is a predicate RR over the dependent product? type

i:IA(i)\prod_{i:I} A(i)

A binary relation over types AA and BB is a predicate \mapsto over the product type A×BA \times B.

See also

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