You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Oscar Cunningham (Apr 15 2020 at 13:58):In HoTT, is there a nice way to phrase the 'Axiom of Choice for sets' that doesn't explicitly refer to sets? Choice is a very useful axiom in lots of contexts, so it seems likely to me that there's some statement about homotopy types which is equivalent to it.
James Wood (Apr 15 2020 at 16:53):The exercises from the HoTT Book chapter 7 seem to talk about various generalisations of choice, but they're all set-indexed (though the choice can be made in higher types). I don't have any insight into why this is.
Oscar Cunningham (Apr 15 2020 at 16:56):I suppose that if we had some statement about general types then to prove it from Choice for sets we would have to use some theorem that allowed us to deduce something about all types using knowledge only about sets. I can't think of any such theorems.