nLab dependent sum natural deduction - table

The inference rules for dependent pair types (aka “dependent sum types” or “ $\Sigma$ -types”):

Last revised on February 15, 2023 at 17:11:55. See the history of this page for a list of all contributions to it.