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