nLab
dependent sum natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
dependent sum typedependent sum
type formationX:Typex:XA(x):Type( x:XA(x)):Type\frac{\vdash\: X \colon Type \;\;\;\;\; x \colon X \;\vdash\; A(x)\colon Type}{\vdash \; \left(\sum_{x \colon X} A\left(x\right)\right) \colon Type}(A p 1 X𝒞)(A𝒞)\left( \array{ A \\ \downarrow^{\mathrlap{p_1}} \\ X} \; \in \mathcal{C}\right) \Rightarrow \left( A \in \mathcal{C}\right)
term introductionx:Xa:A(x)(x,a): x:XA(x)\frac{x \colon X \;\vdash\; a \colon A(x)}{\vdash (x,a) \colon \sum_{x' \colon X} A\left(x'\right) }Q a A x X\array{ Q &\stackrel{a}{\to}& A \\ & {}_{\mathllap{x}}\searrow & \\ && X }
term eliminationt:( x:XA(x))p 1(t):Xp 2(t):A(p 1(t))\frac{\vdash\; t \colon \left(\sum_{x \colon X} A\left(x\right)\right)}{\vdash\; p_1(t) \colon X\;\;\;\;\; \vdash\; p_2(t) \colon A(p_1(t))}Q (x,a) A p 1 X\array{ Q &\stackrel{(x,a)}{\to}& A \\ & & \downarrow^{\mathrlap{p_1}} \\ && X }
computation rulep 1(x,a)=xp 2(x,a)=ap_1(x,a) = x\;\;\;\; p_2(x,a) = aQ (x,a) A x p 1 X\array{ Q &\stackrel{(x,a)}{\to}& A \\ & {}_{\mathllap{x}}\searrow & \downarrow^{\mathrlap{p_1}} \\ && X }
Revised on June 20, 2016 07:18:22 by Matt Earnshaw? (87.81.151.195)