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

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

On 14/06/16 23:30, Michael Shulman wrote:
> Note that the sentence you quoted began with "if MLTT and HoTT refer
> to specific formal systems".  However, as I've been saying, I *don't*
> think "HoTT" should refer to a specific formal system, and you've just
> given one good argument as to why.  (-:

After 50 minutes of reflection, I am not sure how to react to this. 
Whatever the formal system, univalent foundations does start by working 
in a type theory in which types are omega-groupoids and in which there 
is a notion of equivalence which is used to formulate univalence, which 
is postulated.

So I am not sure what you are up to here. Perhaps MLTT was wrong for 
this (univalence). Fair enough. But then we have cubicaltt, which 
accomplishes this and more.

Anyway, I am not sure what is the point you wanted to make.

I am happy for you not to commit yourself to a particular type theory, 
or any theory, but at some point you have to be sufficiently precise 
about what you want to talk about.

> However, I suppose even on the grounds of formal systems one could
> object.  ZF includes Zermelo set theory as a subsystem, but there's no
> reason to say that ZF only "begins" when we start using the
> replacement axiom.  So maybe it would be better to say that, as formal
> systems, MLTT ends when we start using univalence/HITs/etc., but since
> HoTT includes MLTT it begins at the same place.

I guess my point is that MLTT is naturally invariant under equivalence, 
before we postulate the univalence axiom.

In fact, the consistency of the univalence axiom says something about 
MLTT without the univalence axiom: namely that it can't distinguish 
equivalent types.

Martin