nLab
dependent product natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
dependent product typedependent product
type formationX:Typex:XA(x):Type( x:XA(x)):Type\displaystyle\frac{\vdash\: X \colon Type \;\;\;\;\; x \colon X \;\vdash\; A(x)\colon Type}{\vdash \; \left(\prod_{x \colon X} A\left(x\right)\right) \colon Type}(A p 1 p 1 X p 1𝒞)( x:XA(x)𝒞)\left( \array{ A^{\phantom{p_1}} \\ \downarrow^{p_1} \\ X_{\phantom{p_1}}} \in \mathcal{C}\right) \Rightarrow \left( \prod_{x\colon X} A\left(x\right) \in \mathcal{C}\right)
term introductionx:Xa(x):A(x)(xa(x)): x:XA(x)\displaystyle\frac{x \colon X \;\vdash\; a\left(x\right) \colon A\left(x\right)}{\vdash (x \mapsto a\left(x\right)) \colon \prod_{x' \colon X} A\left(x'\right) }
term eliminationf:( x:XA(x))x:Xx:Xf(x):A(x)\displaystyle\frac{\vdash\; f \colon \left(\prod_{x \colon X} A\left(x\right)\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A(x)}
computation rule(ya(y))(x)=a(x)(y \mapsto a(y))(x) = a(x)
Revised on July 8, 2016 17:19:58 by Toby Bartels (108.167.41.14)