[FOM] New umbrella? (Freek Wiedijk)

[Paul Levy]

On 31 Oct 2014, at 19:08, fom-request at cs.nyu.edu wrote:

> Date: Fri, 31 Oct 2014 10:47:24 +0100
> From: Freek Wiedijk <freek at cs.ru.nl>
> To: tchow at alum.mit.edu, Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] New umbrella?
> Message-ID: <20141031094724.GC13928 at wheezy.localdomain>
> Content-Type: text/plain; charset=us-ascii


> On the other hand Coq is much more expressive for abstract
> mathematics (abstract algebra, category theory, etc.) than
> the HOLs

Dear Freek, there's a considerable literature of papers that mix  
category theory and set theory quite seriously.  I recently coauthored  
some papers of this kind* so obviously I'm quite keen on the topic,  
and I'm slightly baffled by the perception of conflict between the two  
subjects.  Some of these papers (not mine) even use large cardinals.

Are you saying there's no suitable proof assistant for formalizing  
results like this?  They're much simpler than the Kepler conjecture  
and Feit-Thompson.

Paul

*The papers are
Coproducts of monads on Set
Exploring the boundaries of monad tensorability on Set
On final coalgebras of power-set functors and saturated trees
available at my publication page
http://www.cs.bham.ac.uk/~pbl/papers/




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