Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
product_type [2014/03/30 19:42] nikolaj |
product_type [2014/03/30 19:42] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Product type ===== | ===== Product type ===== | ||
| ==== Type ==== | ==== Type ==== | ||
| - | | @#55CCEE: context | @#55CCEE: $X, Y, Z$ ... type | | + | | @#55CCEE: context | @#55CCEE: $X, Y$ ... type | |
| | @#FF8866: rule | @#FF8866: ${\large\frac{a\ :\ X\hspace{1cm}b\ :\ Y}{\langle a,b\rangle\ :\ X\times Y}}(\times\mathcal I)$ | | | @#FF8866: rule | @#FF8866: ${\large\frac{a\ :\ X\hspace{1cm}b\ :\ Y}{\langle a,b\rangle\ :\ X\times Y}}(\times\mathcal I)$ | | ||
| | @#FF8866: rule | @#FF8866: ${\large\frac{p :\ X\times Y}{\pi_{\mathcal l}(p)\ :\ X\hspace{1cm}\pi_{\mathcal r}(p)\ :\ Y}}(\times\mathcal E)$ | | | @#FF8866: rule | @#FF8866: ${\large\frac{p :\ X\times Y}{\pi_{\mathcal l}(p)\ :\ X\hspace{1cm}\pi_{\mathcal r}(p)\ :\ Y}}(\times\mathcal E)$ | | ||
