product_type

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,$

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

Logic

Note how the rules reflect the logical “and”.

Parents

Element of

Type