nLab
function type natural deduction - table

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