# nLab function type natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
function typeinternal hom
type formation$\frac{\vdash\: X \colon Type \;\;\;\;\; \vdash\; A\colon Type}{\vdash \; \left(X \to A\right) \colon Type}$
term introduction$\frac{x \colon X \;\vdash\; a(x) \colon A}{\vdash (x \mapsto a\left(x\right)) \colon \left(X \to A\right) }$
term elimination$\frac{\vdash\; f \colon \left(X \to A\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A}$
computation rule$(y \mapsto a(y))(x) = a(x)$

Created on October 2, 2012 at 22:32:21. See the history of this page for a list of all contributions to it.