nLab dependent product natural deduction - table

The inference rules for dependent function types (aka “dependent product types” or “Π\Pi-types”):

Last revised on February 15, 2023 at 18:01:24. See the history of this page for a list of all contributions to it.