[FOM] Wiki: type theoretic fnds

[Lawrence Paulson]

> On 30 Mar 2016, at 21:20, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> What foundational issue is addressed by even ML type theory - no univalence axiom - that cannot be more simply and better addressed by standard f.o.m.?

Let’s state the obvious first: to a constructive mathematician, ZF simply makes no sense. No need to rehearse those arguments here.

But even some classical mathematicians hate having 2 an element of 3 and {a} an element of (a,b). That the intersection of the unit circle with the symmetric group S6 can be formed (even if it’s empty) upsets some people. De Bruijn took this view firmly, and for him, the language of mathematics was full of implicit types. He, more than Martin-Löf, is the godfather of modern type theory. I had the great honour to have meetings with him at Caltech, and it seemed to disappoint him that I went on to work on the formalisation of ZF.

> One of the claimedadvantages of HTT is that it simplifies the treatment of equality. There is an obvious rejoinder to this.

I was being too obscure. The obvious rejoinder is that HTT simplifies something that is difficult in the current popular type theories, but generally straightforward in set theory: reasoning with equalities. 

Larry Paulson