Showing changes from revision #2 to #3:
Added | Removed | Changed
A binary relation over a typetype family is apredicate indexed by a type over is the a product predicate type over the dependent product? type
A relation over a type family indexed by a type is a predicate over the dependent product? type