===== Product type =====
==== 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{p :\ X\times Y}{\pi_{\mathcal l}(p)\ :\ X\hspace{1cm}\pi_{\mathcal r}(p)\ :\ Y}}(\times\mathcal E)$ |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{a\ :\ X\hspace{1cm}b\ :\ Y}{\pi_{\mathcal l}(\langle a,b\rangle)\ \leftrightsquigarrow\ a \hspace{1cm}\pi_{\mathcal r}(\langle a,b\rangle)\ \leftrightsquigarrow\ b}}(\times\beta)$ |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{p\ :\ X\times Y}{\langle\pi_{\mathcal l}(p),\pi_{\mathcal r}(p)\rangle\ \leftrightsquigarrow\ p}}(\times\eta)$ |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{a\ \leftrightsquigarrow\ a'\ :\ X\hspace{1cm}b\ \leftrightsquigarrow\  b'\ :\ Y}{\langle a,b\rangle\ \leftrightsquigarrow\ \langle a',b'\rangle}}$ |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{p\ \leftrightsquigarrow\ p'\ :\ X\times Y}{\pi_{\mathcal l}(p)\ \leftrightsquigarrow\ \pi_{\mathcal l}(p')\hspace{1cm}\pi_{\mathcal l}(p)\ \leftrightsquigarrow\ \pi_{\mathcal r}(p')}}$ |

==== Discussion ====
These are constructors (introduction and elimination), computational rules for $\pi$ (alpha and beta) and defining property of the pair.

== Computational vs. logical point of view ==
Depending on what we want to do with the type system, we might just replace expressions of computational equivalence $\rightsquigarrow$ by equality '$=$'. This symbol denotes a term rewriting, i.e. a computations alla

$\left(\lambda x.\,3+x\right)\,4\ \rightsquigarrow_\beta\ 3+4,$

or

$\lambda x.\,\sin\,x\ \rightsquigarrow_\eta\ \sin$

== Logic ==

Note how the rules reflect the logical "and".
==== Parents ====
=== Element of ===
[[Type]]