Showing changes from revision #0 to #1: Added | Removed | Changed
A binary relation over a type AA is a predicate RR over the product type A×AA \times A
A relation over a type family AA indexed by a type II is a predicate RR over the dependent product? type
dense relation
predicate
proposition
type family
Revision on March 11, 2022 at 20:43:23 by Anonymous?. See the history of this page for a list of all contributions to it.