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:Xx:Xf(x):A\frac{\vdash\; f \colon \left(X \to A\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A}
computation rule(ya(y))(x)=a(x)(y \mapsto a(y))(x) = a(x)
Created on October 2, 2012 22:32:21 by Urs Schreiber (82.169.65.155)