Re: Fibrewise opposite fibration

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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