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”.
Parents
Element of
