Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Martin Escardo <m.es...@cs.bham.ac.uk>]

Thanks, Vladimir for this. It is good to know where you come from, 
explicitly, and what your philosophy and program are.

I will concentrate in one aspect of your reply, which is probably the 
one you didn't intend to emphasize:

On 03/06/16 13:49, Vladimir Voevodsky wrote:
> However the original philosophy of MLTT and the original philosophy of
> UF are different and our use of MLTT for UF is in a sense an abuse of
> the MLTT as Per himself politely mentioned a number of times.

Precisely.

It always seemed to me, for a long time, since the last millemium, that 
the identity type was ad hoc, starting from the fact that there were 
three alternative approaches to patch it:

(1) (Going back to Bishop) Work with setoids.

Perhaps this is *the* philosophy ML had in mind. I don't know. However, 
it is a pity that a formal system supporting this philosophy was 
created, but the philosophy was not formalised by Martin-Loef. But 
Martin Hofmann did this (excluding the universe). Is that what 
Martin-Lof had in mind?

(2) Have the reflection rule. Martin-Loef had this for a while.

But then how does this relate to (1)? I've never seen an account of 
this. People just concentrate on undecidability things regarding (2), 
which I think is a red hearing.

(3) Have the K axiom. This is due to Streicher.

Then UF has a fourth way to look at this:

(4) Certain types do satisfy the K axiom. But there is no reason why all 
types should satisfy it.

What worked as a "revelation" to me what not the univalence axiom (which 
makes (4) good), but something we can say before we consider the 
univalence axiom: although there is no reason to suppose that, in MLTT, 
any two points of Id X x y are themselves Id-related, we have that any 
two points of Sigma(y:X). Id x y are Id-related.

This was known before UF/HoTT, and was considered puzzling for a while. 
What is interesting is that homotopy explains this very clearly and 
naturally. It was this that convinced me that the homotopical view of 
types is correct, once one has identity types. It was not the univalence 
axiom or higher inductive types.

The identity type seemed something at the same time natural and weird 
from the point of view of the philosophy of the last millenium. Without 
changing MLTT, but now looking at it from the homotopical point of view, 
it seems now completely natural to me. Before it felt rather weird.

There is more to say, but I prefer this message to have just one point.

Martin