Hi again,

I should have provided a reference to Rezk's paper -- here is an nLab page with a link and context:

https://ncatlab.org/nlab/show/Global+Homotopy+Theory+and+Cohesion

Some of the ideas go back to Henriques-Gepner, and before that Elmendorf and presumably others, but I'm not intimately familiar with the history. So they are not plucked from the air, but fit into a more recent framework with an explicitly \infty-topos-theoretic slant. That's all I can say for now.

Best regards,
David

On 6 Jun 2016 8:26 pm, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:
When one gives a false mathematical statement I can call it false.

When the statement itself is not mathematical and I believe it to be intentionally misleading I call it a lie. In this particular case it is possible that I was wrong, in which case I apologize. 

I did not notice that the statement was about *a* class of categories. 

It might be the case that geometric representation theorists care about *some* class of (infty,1)-categories that can be obtained by adding "a certain adjoint triple of modal operators” to HoTT (whatever that means). 

In any case the sentence in question is not a mathematical statement and includes a reference to whether or not a certain group of people cares about something.

Vladimir.


On Jun 6, 2016, at 10:32 AM, David Roberts <drobert...@gmail.com> wrote:

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.

--
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.