I assume family here is a function that accepts an index and returns a nonempty set? But then it seems that for the first encountered index the choice function will just return a set rather than an element from it, no? Or am I misreading something?
family is a function that witnesses the “nonemptiness” (really, mere inhabitedness) by returning an element of the propositional truncation of the set. So more formally, axiom_of_choice has type (Πi: I. ||F(i)||) → ||Πi: I. F(i)||. The “choice” comes from the fact that family (due to the propositional truncation) is allowed to return different F(i)’s from identical i’s, whereas choice_fn is required to choose a canonical F(i) for each i . (The intermediate results are untyped because this is a realizer, not a typed term in a type theory.)
😅 This explanation is, I assume, not very helpful to anyone who doesn’t already know what’s going on. But basically in type theory, propositions correspond to (propositionally truncated) types, and proofs correspond to programs/terms with the types in question, so in proving the nonemptiness of the sets, you automatically end up with a witness function that picks out elements—except the witness function may be “nondeterministic” (that’s where the propositional truncation comes in), which is what requires choice to fix.
The propositional truncation is important to understand. There is a version of type theory’s logic that doesn’t include propositional truncation, but in it the axiom of choice is trivial to prove and not really of any use. Unfortunately the intuitive way to explain propositional truncation gives catastrophically wrong intuition for my use-case, as explained here: https://mathstodon.xyz/@MartinEscardo/111014413939196037
I assume
familyhere is a function that accepts an index and returns a nonempty set? But then it seems that for the first encountered index the choice function will just return a set rather than an element from it, no? Or am I misreading something?familyis a function that witnesses the “nonemptiness” (really, mere inhabitedness) by returning an element of the propositional truncation of the set. So more formally,axiom_of_choicehas type(Πi: I. ||F(i)||) → ||Πi: I. F(i)||. The “choice” comes from the fact thatfamily(due to the propositional truncation) is allowed to return differentF(i)’s from identicali’s, whereaschoice_fnis required to choose a canonicalF(i)for eachi. (The intermediate results are untyped because this is a realizer, not a typed term in a type theory.)😅 This explanation is, I assume, not very helpful to anyone who doesn’t already know what’s going on. But basically in type theory, propositions correspond to (propositionally truncated) types, and proofs correspond to programs/terms with the types in question, so in proving the nonemptiness of the sets, you automatically end up with a witness function that picks out elements—except the witness function may be “nondeterministic” (that’s where the propositional truncation comes in), which is what requires choice to fix.
The propositional truncation is important to understand. There is a version of type theory’s logic that doesn’t include propositional truncation, but in it the axiom of choice is trivial to prove and not really of any use. Unfortunately the intuitive way to explain propositional truncation gives catastrophically wrong intuition for my use-case, as explained here: https://mathstodon.xyz/@MartinEscardo/111014413939196037