RE: [HoTT] Identity versus equality

["Joyal, André" <"joyal..."@uqam.ca>]

Dear Thomas,

You are right, the equality of objects in a Grothendieck fibration is judgemental.

Propositional equality of type theory has been studied a lot during the last decades.
I feel quite confortable with it, with the homotopy interpretation and the univalence principle, etc.
I confess that I am much less at ease with judgmental equality and the syntax of type theory.
Until now, type theory has failed to prove that pi_4(S^3)=C_2.
Is it the symptom of a fundamental problem?
Is it because the reduction algoritms are not optimal?
Or because computers are not powerful enough?
What is the abstract theory of terms reduction in type theory?
I apologise for my ignorance.

Best,
André

________________________________________t
From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
Sent: Friday, May 08, 2020 2:40 AM
To: David Roberts
Cc: Joyal, André; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

Dear Robert,

in what I said I didn't mean set theory literally. I was rather referring
to all kinds of categorical logic where equality is interpreted as
(fiberwise) diagonal like (traditional) topos theory in particular.
These kinds of gadgets all have the advantage that "Set" is not ruled
out as a model.

Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.

But this is not my main problem. My main problem is that there is at least
one area of category theory where one has to speak about equality of
objects and these are Grothendieck fibrations. And these are intrinsic
for doing topos theory over general base toposes.
(That I really like them is, admittedly, also an important reason for me
not being ready to give them up! And for reasons of personal and
cultural "antagonisms" they are not very popular among the majority of
category theorists... Thus, there are many people who would not be too
sad about working in a framework not allowing to speak about them.)
But I want to emphasize that real masters of infinite dimensional
categories do not have the faintest problem speaking about equality
when speaking about infinite dimensional versions of Grothendieck
fibrations!)

Though (traditional) topos theory can be developed over fairly general
toposes and this, at least philosophically, is an important aspect one
cannot deny that most toposes of interest heavily rely on Set, be they
of the Grothendieck kind or be they of the realizability kind!

Thomas

PS  Above I put Set into inverted commas because the logician in me
finds it amusing to speak about "the" category of sets which is
nothing but an illusion... Even the nowadays not so little number of
adherents of the "multiverse" view of set theory would share this view!
But even the "universe" view is nothing but an ideology because since
Cohen set theory is mainly a business of constructing different models
via forcing.
Thus, since Set is (sort of) an illusion it is important to do toposes
over arbitrary bases for which purpose one needs Grothendieck fibrations
which do not make sense without equality of objects.

PPS Some people might get the impression I am a "crypto set
theorist". Nothing could be more wrong. I am anti-ideological and
pluralist and I like "deviating" ideas. But I am interested in
calibrating what one needs for which goals. What I am allergic at is
ideological positions which want to forbid someone doing certain
things because they do not fit to some ideological positions...
And one has to accept that not all combinations are possible. Thus
pluralist is better to inegrist!