Re: [HoTT] Identity versus equality

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

In my eyes the reason for the confusion (or rather different views)
arises from the different situation we have in syntax and in semantics.

In syntax the "real thing" is propositional equality and judgemental
equality is just an auxiliary notion. In mathematics it's the well
known difference between equality requiring proof (e.g. by induction) and
checking equality by mere symbolic computation. The latter is just a
technical device and not something conceptually basic.

The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).

This latter view is the view of people working in higher dimensional
category theory as e.g. you, Andr'e when you are not posting on the
list but write your beautiful texts on quasicats, Lurie or Cisinski
(and quite a few others). In these works people are not afraid of
refering to equality of objects, e.g. when defining the infinite
dimensional analogue of Grothendieck fibrations. And this for very
good reasons since there are important parts of category theory where
equality of objects does play a role (typically Grothendieck fibrations).

Fibered cats also often don't allow one to speak about equality of
objects in the base but it is there. This is very clearly expressed so
in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
I think this applies equally well to infinity cats mutatis mutandis.

This phenomenon is not new. Consider good old topos theory. There are
things expressible in the internal logic of a topos and there are
things which can't be expressed in it as e.g. well pointedness or
every epi splits. The first holds vacuously when (misleadingly)
expressed in the internal language of a topos and the second amounts
to so called internal AC (which amounts to epis being preserved by
arbitrary exponentiation). This doesn't mean at all that internal language is
a bad thing. It just means that that it has its limitations...

Analogously, so in infinity category theory. Let us assume for a
moment that HoTT were the internal language of infinity toposes (which
I consider as problematic). There are many things which can be
expressed in the internal language but not everything as e.g. being a
Grothendieck fibration or being a mono...

I mean these are facts which one has to accept. One might find them
deplorable or a good thing but one has to accept them...

One of the reasons why I do respect Voevodsky a lot is that although
he developed HoTT (or better the "univalent view") he also suggested 
2-level type theory when he saw its limitations.

I hope you apologize but I can't supress the following analogy coming
to my mind. After revolution in Russia and the civil war when economy
lay down the Bolsheviks reintroduced a bit of market economy under the
name NEP (at least that's the acronym in German) to help up the economy.
(To finish the story NEP was abandoned by Stalin which lead to well known
catastrophies like the forced collectivization...)

Sorry for that but one has to be careful when changing things and
think twice before throwing away old things...some of them might be
still useful and even indispensible!

Thomas