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

[Vladimir Voevodsky <vlad...@ias.edu>]

[-- Attachment #1.1: Type: text/plain, Size: 5588 bytes --]

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 <mailto: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 <mailto: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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 7865 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]