Re: [HoTT] Identity versus equality

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

Dear Andr'e and Jon,

I mostly agree with what Jon said. I also think that intensional type
theory within an extensional type theory (it is 2 levels and not 3) is
an attractive system for cubical type theory.
In the simplicial case this is a bit more problematic since the
filling conditions for Kan complexes involve classical existential
quantification and as shown by Thierry et.al. this is important!

That the extensional level is just formulated using J and K is a
possibility. It has to be seen in practice how far it goes.

Let me finish with a remark on how constructive traditional topos
theory is. I don't mean the logic represented by a topos but which
logical principles one uses when doing topos theory.
Since one wants to develop toposes relative to fairly general base
toposes people introduced fibered/indexed reasoning. But the reasoning
about fibrations is per se fairly classical and also involves choice
for classes typically. So this reasoning is performed on a meta level
and not within the logic of the base topos. For the situations when
this is partly possible Benabou invented the notion of "definability".

This is sometimes swept under the carpet because of some "antilogical"
tendencies which were influential at the time of the genesis of topos
theory (beautifully described in a little essay by Reyes I recnely
found on his home page). I am aware that I am on dangerous grounds now
since Andr'e has really experienced and shaped these days (when I
started high school).
But it coincides with my impression of what is the practice of the
working topos theorist...

I think the real antagonism is or was that those days (and I am afraid
still nowadays) traditional logicians are mainly adherents of a one
world view. This has changed recently where even among set theorists
there is a "multiverse" and a "universe" fraction and the former is
getting larger compared to the past. This is funny in a sense since
one of the reasons for a multiverse veiw was independnce results is
set theory...

Anyway both traditional topos theory and higher dimensional category
theory was and is developed within a unrestricted metatheory which
could be formalized in ZFC + every set is an element of some Grothendieck universe. 

It is not impossible that certain aspects and fragments can be
developed in weaker systems but there is no guarantee that this will
always work.

Thomas