[FOM] New Umbrella?

[Urs Schreiber]

On 10/26/14, Harvey Friedman <hmflogic at gmail.com> wrote:
> On Sat, Oct 25, 2014 at 6:30 PM, Urs Schreiber
> <urs.schreiber at googlemail.com> wrote:

>> On 10/25/14, Harvey Friedman <hmflogic at gmail.com> wrote in small part:

>>> But there are many convenient
>>> ways of handling situations like this. It's called extra information.
>>> A toy example is f:A into B. Well, the usual way of treating functions
>>> is that f:A into B is equaled to f:A into C if the range is contained
>>> in B and in C. HOWEVER, as you know, you can talk of functions as
>>> pairs (graph(f),B), where you pack the codomain into the function. So
>>> you can introduce special variables for "packed functions" F, and use
>>> the notation dom(F) and codom(F).
>>
>> Hm, this misses the point. Are you familiar with the concept of
>> isomorphism between mathematical structures?
>
> I enjoyed this insult.

Woops. This was not meant as an insult. Sorry. I was just wondering
based on what you wrote. The issue of univalence in HoTT is a simple
statement about ismorphism of types translating into propositional
equality. Given how you were asking and talking about this, I got the
impression you might not know the concept of isomorphism of types.
Sorry apparently you do, then (I don't know your background, I am just
reading here).


> I am going to follow my usual way of proceeding on the FOM when
> somebody offers up some "dramatic new and better way of doing things".

By the way, as far as I can see this, kind of language is used mostly
by you here. I believe it would help your quest for understanding what
the point of HoTT is if you put that aside for a moment and adopted a
more matter-of-fact attitude. After all, HoTT is just an example of a
deductive system. It would seem that of all places, on FOM it should
be possible to discuss some deductive system in a sober way without
feeling threatened by it.

I started my replies to your question of what the point of HoTT is by
saying clearly that the point is that some important high-level part
of modern mathematics is formalized more naturally in HoTT in a way
that makes it more practicable for actual formalization. You keep
saying things that make it sound as if you were debating with somebody
who claimed that HoTT had in-principle advantages over set theory. By
established theorems however [1], this is not so. HoTT is modeled in
ZFC+inaccesbibles and, conversely, (constructive) set theory may be
found in HoTT, so by established theorems one may go back and forth,
subject to some technical fine print.  There is nothing much to be
debated here, it seems to me.


[1] I had given detailed pointers to all these before. Should I recall them?