nLab
dependent sum natural deduction - table

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	dependent sum type	dependent sum
type formation	$\frac{⊢X:\mathrm{Type}x:X⊢A(x):\mathrm{Type}}{⊢\left({\sum }_{x:X}A\left(x\right)\right):\mathrm{Type}}$
term introduction	$\frac{x:X⊢a:A(x)}{⊢(x,a):{\sum }_{x\prime :X}A(x\prime )}$
term elimination	$\frac{⊢t:\left({\sum }_{x:X}A\left(x\right)\right)}{⊢p_1(t):X⊢p_2(t):A(p_1(t))}$
computation rule	$p_1(x,a)=x{p}_2(x,a)=a$