[FOM] New umbrella?

[Bas Spitters]

I think Urs meant "in practice", i.e. in a proof assistant.
Formalizing that paper in, say, Mizar will not be easy (it's quite
technical and uses advanced results in homotopy theory). Moreover, it
only captures one particular higher topos, Kan simplicial sets, not
the general theory.

On Sun, Nov 2, 2014 at 5:51 AM, Monroe Eskew <meskew at math.uci.edu> wrote:
>
> On Nov 1, 2014, at 6:55 PM, Urs Schreiber <urs.schreiber at googlemail.com>
> wrote:
>
> You may tediously
> rebuild that universe inside that tiny corner by building models of
> infinity-toposes in set theory, but this will be immensely tedious and
> is unlikely to be of practical use.
>
>
> Didn’t we already agree that this work has been done?
> http://arxiv.org/pdf/1211.2851v2.pdf
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>