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

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

Definition

A binary relation over a typeAAtype family is apredicateAA indexed by a type R I R I over is the a product predicate type A R×A A R \times A over the dependent product? type

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)
i:IA(i)\prod_{i:I} A(i)

See also

Revision on March 15, 2022 at 07:22:26 by Anonymous?. See the history of this page for a list of all contributions to it.