From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.158.200 with SMTP id ww8mr5301420pab.30.1465020677834; Fri, 03 Jun 2016 23:11:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.17.212 with SMTP id 78ls893537qgd.7.gmail; Fri, 03 Jun 2016 23:11:17 -0700 (PDT) X-Received: by 10.129.154.6 with SMTP id r6mr5368570ywg.55.1465020677345; Fri, 03 Jun 2016 23:11:17 -0700 (PDT) Return-Path: Received: from mail-vk0-x236.google.com (mail-vk0-x236.google.com. [2607:f8b0:400c:c05::236]) by gmr-mx.google.com with ESMTPS id n192si398190vkf.2.2016.06.03.23.11.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 03 Jun 2016 23:11:17 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400c:c05::236 as permitted sender) client-ip=2607:f8b0:400c:c05::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@googlemail.com; spf=pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400c:c05::236 as permitted sender) smtp.mailfrom=urs.sc...@googlemail.com; dmarc=pass (p=QUARANTINE dis=NONE) header.from=googlemail.com Received: by mail-vk0-x236.google.com with SMTP id d127so141241261vkh.2 for ; Fri, 03 Jun 2016 23:11:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=Xu8t6Yesl5nIuDC9B0gVaCQ07z0HOUfHqiuE1SQ3QhI=; b=0Kxw4T5Nz+GT1Kdw9oa7R2z/EXf+EAKHlEPI/0LXnkwMsjA49I0sX7gWBDgxK2pjRw t6SKt9AD4h7YiiVsaEQmFq4f09tJh2kAOanL60DdkKVCCbqQVQWXZH9aysvfwht76cSB zz4S0rpmrpFa0CnPTLmLJ5iadthC7dKG6rEpMNfhQwt6R/W6cLn6uxe5Fp9ffzo6L0rH lLDRZP4kY9iiBBLdgglpkE6Ij5/DW9y7tCpF2YryoowTeEsSt4RK3eke3YpVMMeOD52t CJ49fTfSzzZbdaX5cIL9F+/iHmMy6Bm1cYGb3JcrgFTOvMAmxZVoNAc+o9r9R09mt36J lqcw== X-Gm-Message-State: ALyK8tLpdCgOwQZvmym9vOPG8GomAmiO0faiXm0E5ZBlkZXQB5+dptTIvJZuvMWf25ujDcWyw17SpR+Gg7hVuw== X-Received: by 10.159.33.5 with SMTP id 5mr3405356uab.85.1465020677115; Fri, 03 Jun 2016 23:11:17 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.79.2 with HTTP; Fri, 3 Jun 2016 23:11:16 -0700 (PDT) In-Reply-To: References: <5750A527.4060705@cs.bham.ac.uk> From: Urs Schreiber Date: Sat, 4 Jun 2016 08:11:16 +0200 Message-ID: Subject: Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory? To: Vladimir Voevodsky Cc: Andrew Polonsky , Martin Escardo , Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable > 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