[FOM] New umbrella? (Freek Wiedijk)

[Bas Spitters]

Dear Paul,

Your paper seems somewhat imprecise on what "Set" is. I am guessing
some (Boolean?) topos. Perhaps you need some universes? I'd be
surprised if you were actually using *cumulative* set theory.

I agree with Freek that both Coq and HOL would give you a number of
obstacles to overcome. HoTT (plus classical logic?) may be the most
pleasant framework to actually formalize results like these in, but I
haven't looked at the details.

Best,

Bas

On Fri, Oct 31, 2014 at 10:19 PM, Paul Levy <P.B.Levy at cs.bham.ac.uk> wrote:
>
> 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
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom