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

[Michael Shulman <virit...@gmail.com>]

The main point I meant to make is that I don't know what you mean by
the question "where does MLTT end and HoTT begin?"  I think it could
mean different things, and have different answers, depending on
exactly what one means by "MLTT" and "HoTT" (let alone "begin" and
"end").

But I think this discussion has probably passed the point of
diminishing returns for a mailing list.  (-:  I would be happy to
continue privately if you like.

On Tue, Jun 14, 2016 at 4:33 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
>
> 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