# nLab dependent sum natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
dependent sum typedependent sum
type formation$\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}$$\left(X \in \mathcal{C}, \array{ A \\ \downarrow^{\mathrlap{p_1}} \\ X} \; \in \mathcal{C}/X \right) \Rightarrow \left( A \in \mathcal{C}\right)$
term introduction$\frac{x \colon X \;\vdash\; a \colon A(x)}{\vdash (x,a) \colon \sum_{x' \colon X} A\left(x'\right) }$$\array{ Q &\stackrel{(x,a)}{\to}& A \\ & {}_{\mathllap{x}}\searrow & \\ && X }$
term elimination$\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))}$$\array{ Q &\stackrel{t}{\to}& A \\ & & \downarrow^{\mathrlap{p_1}} \\ && X }$
computation rule$p_1(x,a) = x\;\;\;\; p_2(x,a) = a$$\array{ Q &\stackrel{(x,a)}{\to}& A \\ & {}_{\mathllap{x}}\searrow & \downarrow^{\mathrlap{p_1}} \\ && X }$

Last revised on January 29, 2018 at 15:12:32. See the history of this page for a list of all contributions to it.