Re: Fibrewise opposite fibration

["Jon Sterling" <jon@jonmsterling.com>]

Dear Thomas,

In fact, the reference shows that global choice really is inconsistent in HoTT. Univalence asserts (among other things) that all operations on the universe (even the universe of sets) are "natural" under equivalences, but a global choice operator cannot be natural in this sense.

Best,
Jon


On Tue, Feb 13, 2024, at 10:04 AM, Thomas Streicher wrote:
> Dear Nath and Jon,
>
> I am naturally sympathizing with Nath's remark.
> Thanks, Jon, for giving precise reference for why global choice
> implies classical logic in HoTT (it is not inconsistent as far as I know).
> I am grateful for the quite non-ideological discussion of the issue BTW !
>
> My scepticism w.r.t. HoTT is not ideological (or "self destructive" as
> some people may have thought) but was rather motivated by the fact that it
> caused problems with one of my favourite notions of category theory, namely
> Grothendieck fibrations. There is the notion of Street fibration which
> you obtain when closing Groth. fibrations by closing under categorical
> equivalences. But there are not too many examples as far as I can see.
>
> There is a way out of it suggested by Ahrens and Lumsdaine, namely
> "displayed categories", which are systematically employed in Jon's very
> nice notes on relative category theory with C. Angiuli. This is certainly a way
> how to proceed in case one wants to keep the univalence principle without
> enforcing classical logic.
>
> But it makes things technically more complicated and I personally prefer a
> non-univalent setting. Lurie also can live without univalence both in
> his book and the Kerodon.
> This confirms my impression that univalence is a radical thought experiment
> whose consequences still have to be evaluated. For me (and many other people)
> foundations is not a religious business but rather a question which setting is
> the most convenient one for doing the things one wants to do in maths. This
> can be evaluated only a posteriori and a certain pluralism might be a healthy
> attitude.
>
> In any case I think w.r.t. fibered categories the most reasonable thing
> seems to be cleaved fibrations and arbitrary cartesian functors. It is
> foundationally tolerant and close to the practice of fibered category theory.
>
> Thomas



----------

You're receiving this message because you're a member of the Categories mailing list group from Macquarie University.

Leave group:
https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b