Dear Nath,

It is important to note that although global choice is a very useful tool indeed, it is not consistent with the interpretation of the universe of sets in univalent foundations (UF) — despite the fact that the usual axiom of choice can be added to univalent foundations without any problems. The contradiction is described in Theorem 3.2.2 of the HoTT Book.

Of course, one is free to use traditional set theoretic foundations (either in terms of ZFC, or in terms of its embedding into UF + choice via iterative notions of set), and in this case the usual classical results about the consistency of indefinite descriptions would be available — but the reason I bring this up is that univalent foundations offers a compelling alternative to the usual approach of filling in missing data via choice that you bring up. In set theoretic foundations, the missing data is not uniquely determined (it is only unique up to isomorphism) and so you need some kind of choice to get it back; but in univalent foundations, it very often (in fact, usually!) happens that this missing data is uniquely determined in the appropriate sense — in this way, univalence increases the scope of *definite* descriptions so much that many classical uses of choice and/or indefinite descriptions become obsolete. This is why, in univalent foundations, you can avoid choosing a cleaving of a fibration because all fibrations are automatically, canonically, cloven.

It makes sense that there is a variety of approaches to deal with such issues.

Best,
Jon


On Mon, Feb 12, 2024, at 1:20 PM, Nath Rao wrote:
> [This no longer about how to define fibrewise opposite fibration, so may
> be it is time t change the subject line.]
>
> IMHO, this seems to be more like a religious war. In "mathematics in the
> small", local axiom of choice allows us to choose representatives only
> when needed. So we are grew up believing that putting things in the
> definition that are not preserved by morphisms is "not done" (the
> religious dogma) . But them we run up against issues when we try to do
> the same thing in "mathematics in the large", and either ignore the
> problem or argue endlessly about how to solve it.
>
> Also, if are willing to assume that every set comes with a
> well-ordering, why not assume a global well-ordering and be done with
> it? [If I am going to use universes anyway, it seems to be trivial to do
> this, as long as I live inside a fixed universe in any given proof.] For
> ZFC, global choice is a conservative extension. Not being a logician, am
> not sure, but perhaps it can be shown for global choice is a
> conservative extension of local choice of 'all suitable set theories'.
> Then we can do global choice with no qualms.
>
> Regards
> Nath Rao
>
>
>
>
>
> ----------
>
> You're receiving this message because you're a member of the Categories 
> mailing list group from Macquarie University.
>
> Leave group:
> https://protect-au.mimecast.com/s/Uy0cCp81gYC8WpnQSP-lCQ?domain=outlook.office365.com