Bartosz Milewski on Nostr: Axiom of Choice in HoTT. For any family of sets Y parameterized by elements of a set ...

Axiom of Choice in HoTT. For any family of sets Y parameterized by elements of a set X, there exists a function below.

Naively, this says that if all sets Y(x) are inhabited then all sets Y(x) are inhabited. Duh!

The tricky part is the vertical bars. They signify 'propositional truncation', meaning: we know it's true, but we forgot why. So we know that every Y(x) is not empty, but we don't have the witness of this fact.

The axiom of choice says that the witnesses exist: if you know that the sets are non-empty, it's possible to choose one element from each set.

The propositional truncation on the right means that, trust me!, the witnesses exist, but you can't get at them.