The principle of finite choice states that the dependent product of a finite family of inhabited sets is itself inhabited.
Finite choice is provable in most set theories, including strongly predicative and constructive set theories, as well as set theories without quotient sets.
In dependent type theory, finite choice is definable and provable, provided one has identity types, dependent sum types, bracket types, finite sets, and dependent tuple types in the type theory:
One could express the principle of finite choice as two separate cases representing the case with zero and two inhabited sets:
Every singleton is an inhabited set
The product of two inhabited sets is inhabited.
In dependent type theory, the former follows from the definition of a singleton or contractible type as an inhabited mere proposition, and the latter is given by the following rule:
Last revised on January 10, 2023 at 13:56:48. See the history of this page for a list of all contributions to it.