Homotopy Type Theory relation > history (changes)

Showing changes from revision #7 to #8: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~
~~A relation over a type family $A$ indexed by a type $I$ is a predicate $R$ over the dependent product? type~~
~~$\prod_{i:I} A(i)$~~
~~A binary relation over types $A$ and $B$ is a predicate $\mapsto$ over the product type $A \times B$ .~~
~~See also~~

directed graph

predicate

proposition

type family

~~category: not redirected to nlab yet~~

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