[FOM] Wiki: type theoretic fnds

[David McAllester]

>
>
>
> 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.
>
​
But the issue is the relationship between absolute equality (
set-theoretic equality) and the common-sense notion of isomorphism between
structures. Reasoning with set-theoretic equality only does not solve this
problem.

David
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160401/d81fa469/attachment.html>