[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
>
> Dear Paul,
>
> Your paper seems somewhat imprecise on what "Set" is. I am guessing
> some (Boolean?) topos.

These papers generally need excluded middle, Axiom of Choice and Axiom  
of Replacement, so I don't believe the results would apply to an  
arbitrary boolean topos.

> Perhaps you need some universes?

We can make do with classes (since functor categories from large  
categories aren't used), but life is easier with universes.

> I'd be surprised if you were actually using *cumulative* set theory.

You are right; these papers don't depend on Foundation.

A famous example: every endofunctor F on Set preserving injections is  
isomorphic to one preserving inclusions.  (Adamek)

This follows from either global choice or strong extensionality (the  
statement that any two bisimilar sets are equal, implied by Foundation  
and by Antifoundation).

Antifoundation, while we're on the subject, is so much fun.  For  
example, it implies that domain equations have unique identity- 
structured bifree solutions.

Too bad there will be no place for fun in the serious mathematics of  
the future.  :-(

Paul


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