Product 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')}}$


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$


Note how the rules reflect the logical “and”.


Element of

Link to graph
Log In
Improvements of the human condition