[FOM] HoTT unresponsiveness

[Paul Levy]

> Date: Sun, 26 Oct 2014 22:41:04 -0400
> From: Joseph Shipman <JoeShipman at aol.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: [FOM] HoTT unresponsiveness
> Message-ID: <22A397EE-B833-47C8-9933-F7C413EC9CD5 at aol.com>
> Content-Type: text/plain;	charset=us-ascii

> 4a) is there any theorem in HoTT, no reasonable equivalent of which  
> can be STATED in ZFC?

"Every endofunction on the universe of sets extends to an endofunctor  
on the groupoid of sets and bijections."

This statement is PROVABLE in HoTT and some other systems.

It is REFUTABLE in ZF with universes, NBG and some other systems.

Take your pick.  Personally I prefer it not to be a theorem, but I can  
understand why some people would take a different view.  It's a tricky  
philosophical question about the very nature of sets.

Paul


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