From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.140.154.68 with SMTP id a65mr11913930qha.29.1465198335642; Mon, 06 Jun 2016 00:32:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.44.135 with SMTP id i129ls570554iti.35.gmail; Mon, 06 Jun 2016 00:32:15 -0700 (PDT) X-Received: by 10.66.254.34 with SMTP id af2mr11958572pad.12.1465198335039; Mon, 06 Jun 2016 00:32:15 -0700 (PDT) Return-Path: Received: from mail-it0-x22b.google.com (mail-it0-x22b.google.com. [2607:f8b0:4001:c0b::22b]) by gmr-mx.google.com with ESMTPS id y11si606725itf.2.2016.06.06.00.32.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 06 Jun 2016 00:32:14 -0700 (PDT) Received-SPF: pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:4001:c0b::22b as permitted sender) client-ip=2607:f8b0:4001:c0b::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:4001:c0b::22b as permitted sender) smtp.mailfrom=drobert...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x22b.google.com with SMTP id f67so35808716ith.1 for ; Mon, 06 Jun 2016 00:32:14 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc; bh=yYmQgfRePd9nXUeC8e703lqllxkFz3Ep52EfDRRBIT4=; b=bOr8CNz1gCJBi6Ax1d7CT2M2uQ8rDC2OjqlqChnF8AfMcsHyfGrxs1U0inI/LbY1P+ br8z7M3vxwJS8t//U7VqPBa5jRVASIYcLwSZVWTRqoc4PSCRpn/U2Uw2x0KRMEi/pmU0 1W9+Nic7Zrlf3TnItdAfhdn4DZnMsWOZuJZ1h7dlfqdytfAu4Cp7P/tjRLmhsbQHpjfY OjvmIMVr0j1tdt4KzMv4Ub+IqdfwpTJschAJyziycs4CCX2mpRWIVlVPSt7xNYN97CsZ htPFSlFOFJXnXGuQN1bs4OG5y8crTRRlVB4QAhzJoSVNduc+cf5V0A2+R3IahYzYqK9r 7xdA== X-Gm-Message-State: ALyK8tJlEIZK42iCyWtSe2DXzCRXXU2ukxswZ8dXqc4+BoibO38ArGsWKHmBAf8UmvmAVNXwDrN6loQ6NBIzqQ== MIME-Version: 1.0 X-Received: by 10.36.50.10 with SMTP id j10mr14962232ita.27.1465198334818; Mon, 06 Jun 2016 00:32:14 -0700 (PDT) Received: by 10.107.26.68 with HTTP; Mon, 6 Jun 2016 00:32:14 -0700 (PDT) Received: by 10.107.26.68 with HTTP; Mon, 6 Jun 2016 00:32:14 -0700 (PDT) In-Reply-To: <7AC24044-EDEF-4490-BC72-24885504B619@ias.edu> References: <5750A527.4060705@cs.bham.ac.uk> <7AC24044-EDEF-4490-BC72-24885504B619@ias.edu> Date: Mon, 6 Jun 2016 17:02:14 +0930 Message-ID: Subject: Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory? From: David Roberts To: Vladimir Voevodsky Cc: homotopytypetheory , Urs Schreiber , Martin Escardo , Andrew Polonsky Content-Type: multipart/alternative; boundary=001a114ab04e45c13005349712bd --001a114ab04e45c13005349712bd Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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" 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)-categor= y. > > Vladimir. > > > > > > > On Jun 4, 2016, at 9:11 AM, Urs Schreiber > wrote: > > > >> They don=E2=80=99t 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. > --001a114ab04e45c13005349712bd Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

Dear Vladimir,

Please see Charles Rezk's work on globally equivariant h= omotopy theoretic models of cohesion. It is not something out of Urs' i= magination.

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

Best regards,
David

On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky&= quot; <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=E2=80=99t take us seriously so far because we can not def= ine
>> (infty,1)-categories.
>
> The good news is, without even having to define them, HoTT already is<= br> > 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<= br> > 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<= br> > 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<= br> > 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<= br> > 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--001a114ab04e45c13005349712bd--