Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[David Roberts <drobert...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4226 bytes --]

Dear Vladimir,

Please see Charles Rezk's work on globally equivariant homotopy theoretic
models of cohesion. It is not something out of Urs' imagination.

Also, if something is false, call it false, not a 'lie', and provide a
mathematical basis for such a statement.

Best regards,
David
On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:

> Dear Urs,
>
> > For instance a class of (infinity,1)-categories that geometric
> > representation theorists care about is neatly obtained in HoTT by just
> > adding a certain adjoint triple of modal operators (differential
> > cohesion)
>
> this is a lie.
>
> Geometric representation theorists care about the (infty,1)-categories
> that corresponds to different groups and to their interaction with each
> other. They care not about sitting inside one universal (infty,1)-category.
>
> Vladimir.
>
>
>
>
>
> > On Jun 4, 2016, at 9:11 AM, Urs Schreiber <urs.sc...@googlemail.com>
> wrote:
> >
> >> They don’t take us seriously so far because we can not define
> >> (infty,1)-categories.
> >
> > The good news is, without even having to define them, HoTT already is
> > the internal language of certain (infinity,1)-categories. Which ones
> > precisely depends on which axioms are added or omitted.
> >
> > For instance a class of (infinity,1)-categories that geometric
> > representation theorists care about is neatly obtained in HoTT by just
> > adding a certain adjoint triple of modal operators (differential
> > cohesion) This yields a synthetic axiomatization of the homotopy
> > theory of D-modules and their representation theory, which is what is
> > mostly meant by "geometric representation theory".
> >
> > This route is the homotopy version of Lawvere's seminal vision of all
> > mathematics taking place synthetically inside a suitable elementary
> > topos. It's slightly ironic that this route is not more popular.
> > Because over in the community of ordinary (i.e. non-type theoretic)
> > infinity-category theory, there is the nagging feeling that handling
> > all those incarnations of infinity categories as simplicial and n-fold
> > simplicial objects from the outside may be rather inefficient for
> > deriving results. In order to overcome this there is the work on
> > derivators and the work by Riehl-Verity.
> >
> > A colleague of mine championing derivators praises the fact that they
> > offer him a formal way to verify the simplicial reasoning in work by
> > Lurie et al, which he finds intricate to the point of being
> > unverifiable to him. This certainly applies to other people, too.
> >
> > To check this, you should do a survey among your colleagues whether or
> > not they think that Lurie actually gave a proof of the cobordism
> > hypothesis. Lurie gives an intriciate argument in terms of
> > infinity-categories modeled on simplicial set, and while I fully trust
> > that it is correct, it is true that it gets to the point of compexity
> > where it seems that checking the proof is not just a matter of
> > mchanically checking derivation steps, but requires extra ingenuity.
> >
> > Now, HoTT, regarded as an internal language, shares with the concept
> > of derivators the potential to make much of this somewhat
> > messy-looking simplicial infinity-category theory become more
> > transparent and systematic, more mechanical. Therefore it might be
> > argued to be a little be backwards to try to force that messy
> > simplicial technology to realize itself inside HoTT. It might be
> > missing the golden opportunity to turn this around and use the
> > synthetic reasong.
> >
> > There is now one person, Felix Wellen, working on formalizing some
> > first basics of geometric representation theory within differentially
> > cohesion HoTT. I think it's a topic with plenty of opportunity.
> >
> > Best wishes,
> > urs
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 5075 bytes --]