From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a92:1949:: with SMTP id e9mr13473643ilm.106.1589142171673; Sun, 10 May 2020 13:22:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:3007:: with SMTP id q7ls1298376jaq.4.gmail; Sun, 10 May 2020 13:22:50 -0700 (PDT) X-Received: by 2002:a05:6638:ca6:: with SMTP id x6mr9767154jad.131.1589142170382; Sun, 10 May 2020 13:22:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589142170; cv=none; d=google.com; s=arc-20160816; b=hnaatfYQkfDZgvxcLPsfUTuws1lGEVKPsOUhjcdeCG/PG3jSRTJqSgJVkVvXggklIN PNXkAYhktEIE9TlyK3tK7CfNq3od+wPnWCNUtazmEZQ/HU91+g6VrqWrCq7Kdaf2yV/c OZJeuOqoTk8SvWTBgPk7UZlCOUnygaV3yY4HUoAXQadmo1u3eTJL75+Z6Y8T1WI72R9D dWSQmd6djCbQu4I6CiYwMPLOOVyxxCJTvXxfK0xewlZ5C1hQuX+8rNDcyz8hyp4RHmki GKu55PD1xZFdgoJ/pdru2QJLQzY+qCdH2GNCg9nylT5uOcvsiO/S9dY4fQcbC6DlWQye sJgg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=uGxa9JUBKJhNk2/a5h8VM8stOeUeUZ2EJkgHJc88p1o=; b=gPP9w0bZbHOxJrMamI/uwhWdH0Ao4SfYBXhfUFOEGrNABy9Xg3Strfx3IX2K46Dlbi YkMVSAhD8CC4eD+sL7CkQvi3AxnZCECaqrNPvTdnvD0vUQnKJWRIdwCXEuCtzMgCYRi0 THP/el+6hh0TYS7r5cVcTIrxDR9HapHv5HM3ape5O4r+XWW55WoKXkmjILcpzp/AX/6/ VDFHIxpFNtgMcwFCvyUjTvOmNKsUYuVDNkmu0AzqjIgiqIrR8zl+8JKZM84wlivteAmr wojwPvM2G3fjZp+zpbga1EpetrbyHOhEHhVbcTDfaqMtPyg1rhrd6HP33/GXh/x0mTsv ryWg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Xn4xPCMk; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::22f as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-oi1-x22f.google.com (mail-oi1-x22f.google.com. [2607:f8b0:4864:20::22f]) by gmr-mx.google.com with ESMTPS id k74si25178ila.1.2020.05.10.13.22.50 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 13:22:50 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::22f as permitted sender) client-ip=2607:f8b0:4864:20::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Xn4xPCMk; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::22f as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-oi1-x22f.google.com with SMTP id t199so13429730oif.7 for ; Sun, 10 May 2020 13:22:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=uGxa9JUBKJhNk2/a5h8VM8stOeUeUZ2EJkgHJc88p1o=; b=Xn4xPCMkPKUHNA5yrnu0REsf/DVLk6EsiRwX4xJf0/LRrCAMadfmCW1VuxDPLbx+r8 OI8OFLxIX6/HRsBwrK9SX1zApluYyWuPt1qafKo6hDHvtdyjUKmSYM6DNfKtH1rc06f/ 3mfsWAbgwKribvmcWJH3H1LN7yqgXI+po/h3YTMn9wC7QEQMF+emPgkdGCZQAzMF0oAx soOMJhzhlcmh12Achswbik7+g5mYLWydbZnmg7Qu2nE5m5oHiTu1hnJ4/Uev5U+oZhjx W+QNWWXV/r+mY1/cj5SBRVTjioZw/C5B4PgKF66T1jc6gAqw9PIx3La2psHyjaxtckL3 LFdg== X-Gm-Message-State: AGi0Puann1sMvOuFYl5te+ZYbcOuQ08s+TYuTZn0D45rS5SQkTNIaHKn Hpf7o2Gamr6aKuYUebE+1MGSYH3Hd8PY/92DU9hTj6GpGBhASeSsfRq9oqice4t3aFdcgxFn1tl QqnM5dnszq0Pb2QA9UIFQsdI1aJLqGE/eHC3uJhr8OBHPZLcY6dhY87eilvqFDCiIMEk3ghue4L r3ljvgI4N2 X-Received: by 2002:a05:6808:4d5:: with SMTP id a21mr12682532oie.105.1589142169752; Sun, 10 May 2020 13:22:49 -0700 (PDT) Return-Path: Received: from mail-oi1-f174.google.com (mail-oi1-f174.google.com. [209.85.167.174]) by smtp.gmail.com with ESMTPSA id l26sm295232oos.43.2020.05.10.13.22.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 13:22:48 -0700 (PDT) Received: by mail-oi1-f174.google.com with SMTP id r66so13400097oie.5 for ; Sun, 10 May 2020 13:22:48 -0700 (PDT) X-Received: by 2002:aca:f541:: with SMTP id t62mr16967489oih.148.1589142168516; Sun, 10 May 2020 13:22:48 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> In-Reply-To: From: Michael Shulman Date: Sun, 10 May 2020 13:22:35 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Nicolai Kraus Cc: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , Thomas Streicher , David Roberts , Thorsten Altenkirch , Steve Awodey , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I'm not sure I understand the meanings of "deep" and "shallow" completely, but the dichotomy seems similar to what we sometimes call "analytic" and "synthetic". Any foundational theory only directly/synthetically represents a few concepts; all others have to be encoded into it "analytically". In ZFC, the synthetic objects are well-founded membership structures; in ETCS the synthetic objects are featureless point-sets and functions; in HoTT the synthetic objects are oo-groupoids. It seems reasonable to me to argue that whenever we use the fundamental objects of the framework we should treat them synthetically, but not expect any other structures to be synthetic. When working in ZFC, it would be perverse to constantly work with well-founded membership structures rather than simply use sets. And when working in HoTT, it would be perverse to work with oo-groupoids defined in terms of set rather than simply use types. But neither ZFC nor HoTT has a synthetic notion of "simplicial oo-groupoid" or "oo-category", so in both cases those structures have to be defined analytically -- the only difference is that the oo-groupoid "ingredients" are in ZFC themselves analytic whereas in HoTT those ingredients are synthetic. On Sun, May 10, 2020 at 12:18 PM Nicolai Kraus wrote: > > In the last paragraph of my message below, the words "deep" and "shallow"= have to be swapped. > > On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus wrote= : >> >> Dear Andr=C3=A9 and everyone, >> >> I feel it's worth pointing out that there are two strategies to express >> "everyday mathematics" in HoTT. In CS-speak, they would probably be >> called "shallow embedding" and "deep embedding". Shallow embedding is >> the "HoTT style", deep embedding is the "pre-HoTT type theory style". >> Shallow means that one uses that the host language shares structure with >> the object one wants to define, while deep means one doesn't. To explain >> what I mean, let's look at the type theoretic definition of a group (a >> 1-group, not a higher group). >> >> Definition using deep embedding: A group is a tuple >> (X,h,e,o,i,assoc,...), where >> X : Type -- carrier >> h : is-0-truncated(X) -- carrier is set >> e : X -- unit >> o : X * X -> X -- composition >> i : X -> X -- inverses >> assoc : (h o g) o f =3D h o (g o f) >> ... [and so on] >> >> Definition using shallow embedding: A group is a pointed connected 1-typ= e. >> >> Fortunately, these definitions are equivalent (via the Eilenberg-McLan >> spaces construction). But they behave differently when we want to work >> with them or change them. It's easy to change the second definition to >> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 , >> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there >> is a nice way for the first definition. The second definition has better >> computational properties than the first. >> >> When you say this: >> >> > But I find it frustrating that I cant do my everyday mathematics with= it. >> > For example, I cannot say >> > >> > (1) Let X:\Delta^{op}---->Type be a simplicial type; >> >> You are referring to shallow embedding. In everyday mathematics, you >> don't say (1) either. You probably say (1) with "Type" replaced by "Set" >> or by "simplicial set". Both of these can be expressed straightforwardly >> in type theory using only (h-)sets (i.e. embedding deeply). >> >> We strive to use shallow embedding as often as possible for the reasons >> in the above example. But let's assume that we *can* say (1) in HoTT, >> using "Type", because we find some encoding that we're reasonably happy >> with; there's a question which I've asked myself before: >> >> Will we not destroy the advantages of deep (over shallow) embedding if >> we fall back to encodings (and thus destroy the main selling point of >> HoTT)? For me, the justification of still using deep embedding is that >> statements using encodings (e.g. "the universe is a higher category) >> might still imply statements which don't use encodings and are >> interesting. However, if we want to develop a theory of certain higher >> structures for it's own sake, then it's not so clear to me whether it's >> really better to use the HoTT-style deep embedding. >> >> Kind regards, >> Nicolai >> >> >> On 09/05/2020 21:18, Joyal, Andr=C3=A9 wrote: >> > Dear Thomas, >> > >> > You wrote >> > >> > <> > for proving and not for computing. >> > But if you haven't mechanized PART of equational reasoning it would be >> > much much more painful than it still is. >> > But that is "only" a pragmatic issue.>> >> > >> > Type theory has very nice features. I wish they could be preserved an= d developped further. >> > But I find it frustrating that I cant do my everyday mathematics with = it. >> > For example, I cannot say >> > >> > (1) Let X:\Delta^{op}---->Type be a simplicial type; >> > (2) Let G be a type equipped with a group structure; >> > (3) Let BG be the classifying space of a group G; >> > (4) Let Gr be the category of groups; >> > (5) Let SType be the category of simplical types. >> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y >> > between two simplicial types X and Y. >> > >> > It is crucial to have (1) >> > For example, a group could be defined to >> > be a simplicial object satisfying the Segal conditions. >> > The classifying space of a group is the colimit of this simplicial obj= ect. >> > The category of groups can be defined to be >> > a simplicial objects satisfiying the Rezk conditions (a complete Segal= space). >> > >> > Is there some aspects of type theory that we may give up as a price >> > for solving these problems ? >> > >> > >> > Best, >> > Andr=C3=A9 >> > >> > ________________________________________ >> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] >> > Sent: Saturday, May 09, 2020 2:43 PM >> > To: Joyal, Andr=C3=A9 >> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;= homotopyt...@googlegroups.com >> > Subject: Re: [HoTT] Identity versus equality >> > >> > Dear Andr'e, >> > >> >> By the way, if type theory is not very effective in practice, why do = we insist that it should always compute? >> >> The dream of a formal system in which every proof leads to an actual = computation may be far off. >> >> Not that we should abandon it, new discoveries are always possible. >> >> Is there a version of type theory for proving and verifying, less >> >> for computing? >> > In my opinion the currenrly implemented type theories are essentially >> > for proving and not for computing. >> > But if you haven't mechanized PART of equational reasoning it would be >> > much much more painful than it still is. >> > But that is "only" a pragmatic issue. >> > >> >> The notations of type theory are very useful in homotopy theory. >> >> But the absence of simplicial types is a serious obstacle to applicat= ions. >> > In cubical type theory they sort of live well with cubes not being >> > fibrant... They have them as pretypes. But maybe I misunderstand... >> > >> > Thomas >> > >>