dependent sum natural deduction - table

type theorycategory theory
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}(X𝒞,A p 1 X𝒞/X)(A𝒞)\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 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 (x,a) A x X\array{ Q &\stackrel{(x,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 t A p 1 X\array{ Q &\stackrel{t}{\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 }

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