[FOM] New Umbrella?

[Monroe Eskew]

> On Oct 27, 2014, at 6:23 AM, Urs Schreiber <urs.schreiber at googlemail.com> wrote:
> 
> 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.

This point should ultimately eliminate any advantage in formalization that HoTT has over set theory.  If we want our mathematics to be completely formalized in the official language of set theory, with the ZFC axioms and some mild large cardinals, and the deduction rules of FOL, then we only need to complete one project in order to co-opt all the formal advantages of HoTT.  Just produce a formal proof that ZFC+inaccessibles (naturally) interprets HoTT, and then apply this result to any future deductions from HoTT.  Maybe this is actually worth doing!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141028/efc36b3a/attachment.html>