nLab
dependent product natural deduction - table

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	dependent product type	dependent product
type formation	$\frac{⊢X:\mathrm{Type}x:X⊢A(x):\mathrm{Type}}{⊢\left({\prod }_{x:X}A\left(x\right)\right):\mathrm{Type}}$
term introduction	$\frac{x:X⊢a\left(x\right):A\left(x\right)}{⊢(x\mapsto a\left(x\right)):{\prod }_{x\prime :X}A(x\prime )}$
term elimination	$\frac{⊢f:\left({\prod }_{x:X}A\left(x\right)\right)⊢x:X}{x:X⊢f(x):A(x)}$
computation rule	$(y\mapsto a(y))(x)=a(x)$