nLab function type natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
function typeinternal hom
type formationX:TypeA:Type(XA):Type\frac{\vdash\: X \colon Type \;\;\;\;\; \vdash\; A\colon Type}{\vdash \; \left(X \to A\right) \colon Type}
term introductionx:Xa(x):A(xa(x)):(XA)\frac{x \colon X \;\vdash\; a(x) \colon A}{\vdash (x \mapsto a\left(x\right)) \colon \left(X \to A\right) }
term eliminationf:(XA)x:Xf(x):A\frac{\vdash\; f \colon \left(X \to A\right)\;\;\;\; \vdash \; x \colon X}{\;\;\;\vdash\; f(x) \colon A}
computation rule(ya(y))(x)=a(x)(y \mapsto a(y))(x) = a(x)

Last revised on September 29, 2018 at 19:47:09. See the history of this page for a list of all contributions to it.