[FOM] New umbrella?

[Paul Levy]

On 2 Nov 2014, at 17:05, fom-request at cs.nyu.edu wrote:
> Date: Sun, 2 Nov 2014 13:26:21 +0100
> From: Bas Spitters <b.a.w.spitters at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Cc: Freek Wiedijk <freek at cs.ru.nl>
> Subject: Re: [FOM] New umbrella? (Freek Wiedijk)
> Message-ID:
> 	<CAOoPQuTo1RoPwDQwQwwixVTX4ioTvnAuDQRVG+D=g2DFof72qg at mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8

>  HoTT (plus classical logic?) may be the most
> pleasant framework to actually formalize results like these in

I think that's impossible.  Surely one cannot embed ZFC + universes  
into HoTT, because HoTT refutes choice over a universe.

Paul


--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
http://www.cs.bham.ac.uk/~pbl