Abstract
The Axiom of Choice (AC) is a principle of set theory and logic stating that given a collection of non-empty sets, it is possible to derive a function that selects exactly one element from each set. In Type Theory and Homotopy Type Theory, the status of this principle is nuanced: while a version of it is a theorem in Type Theory, the version involving propositionally truncated types is an nonconstructive axiom.
Idea
The Axiom of Choice is a logical principle that allows for a choice function to be obtained from a mere existence of witnesses in each fiber.
In constructive type theory, the “internal” version of choice is often a tautology because a proof of already consists of a function and a proof of its correctness. However, when is interpreted as the propositional truncation , the principle becomes non-trivial.
Definition
The most general choice is of the following form:
In the context of hott2013-book, this is typically formulated for sets (0-types) and and a family of mere propositions :
Other Choice Principles
Choice principles are often categorized by the constraints placed on the domain or the strength of the existence claim.
Cardinality-Based Choice
A choice principle is classified by the maximum cardinality that may have:
- Finite Choice: When is a finite type.
- Countable Choice: When is the type of natural numbers or any countable type.
Weakly-Initial Set of Covers
- WISC: A much weaker choice principle than the full Axiom of Choice. It states that for every type , there exists a Set and a family of surjections that cover the collection of all surjections into .
Properties
- Diaconescu’s Theorem: In many type theories, the Axiom of Choice implies the Law of Excluded Middle ().
- Function Extensionality: The type-theoretic version of AC often interacts with Function Extensionality to determine the behavior of universes.