This is an old revision of the document!

Product type

Type

 context $X, Y$ … type rule ${\large\frac{a\ :\ X\hspace{1cm}b\ :\ Y}{\langle a,b\rangle\ :\ X\times Y}}(\times\mathcal I)$ rule ${\large\frac{p :\ X\times Y}{\pi_{\mathcal l}(p)\ :\ X\hspace{1cm}\pi_{\mathcal r}(p)\ :\ Y}}(\times\mathcal E)$ rule ${\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)$ rule ${\large\frac{p\ :\ X\times Y}{\langle\pi_{\mathcal l}(p),\pi_{\mathcal r}(p)\rangle\ \leftrightsquigarrow\ p}}(\times\eta)$ rule ${\large\frac{a\ \leftrightsquigarrow\ a'\ :\ X\hspace{1cm}b\ \leftrightsquigarrow\ b'\ :\ Y}{\langle a,b\rangle\ \leftrightsquigarrow\ \langle a',b'\rangle}}$ rule ${\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”.