nLab
product natural deduction - table

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	product type	product
type formation	$\frac{⊢A:\mathrm{Type}⊢B:\mathrm{Type}}{⊢A\times B:\mathrm{Type}}$	$A,B\in 𝒞\Rightarrow A\times B\in 𝒞$
term introduction	$\frac{⊢a:A⊢b:B}{⊢(a,b):A\times B}$	$\begin{array}{ccc}& & Q\\ & {}^a\swarrow & {\downarrow }_{(a,b)}& {\searrow }^b\\ A& & A\times B& & B\end{array}$
term elimination	$\frac{⊢t:A\times B}{⊢p_1(t):A}\frac{⊢t:A\times B}{⊢p_2(t):B}$	$\begin{array}{ccc}& & Q\\ & & {\downarrow }^t& & \\ A& \stackrel{p_1}{\leftarrow }& A\times B& \stackrel{p_2}{\to }& B\end{array}$
computation rule	$p_1(a,b)=a{p}_2(a,b)=b$	$\begin{array}{ccc}& & Q\\ & {}^a\swarrow & {\downarrow }_{(a,b)}& {\searrow }^b\\ A& \stackrel{p_1}{\leftarrow }& A\times B& \stackrel{p_2}{\to }& B\end{array}$