From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.4 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,NICE_REPLY_A, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 31899 invoked from network); 4 Mar 2021 22:42:36 -0000 Received: from mail-wr1-x43b.google.com (2a00:1450:4864:20::43b) by inbox.vuxu.org with ESMTPUTF8; 4 Mar 2021 22:42:36 -0000 Received: by mail-wr1-x43b.google.com with SMTP id r12sf139573wro.15 for ; Thu, 04 Mar 2021 14:42:36 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614897753; cv=pass; d=google.com; s=arc-20160816; b=lWlhwdFs8Ed0xD9E1l7GCoL205BK3i3+KjWGYi035vUCJLtH7qbH9vHorTVQ3zAuYM zNWSiQijUPisNvHHO+nXWnNrCBrk2x3DQTIrW7db8AJ0PX7Q3n7W6GbCj/eH66GGz6qx ww/ocfjRVMumX/0VXc9xzs+71vhagacqizcVSyfYIyfZs7FOskpL5U0p2U1wHs1ggFDA OXuqu0HeJNUNQT3nDKNaSSXdX74L+NJX3f2CUK+XZ4l9ju01jsWGzZF8wuJnH9Uvt/Gx +9e8teiDKtH+ewNtqF+TwnSsEM58EzPxIpPW2Mgiv4ivs4yKX/q4M9Mc+19w70b/3iBy qwGA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :cc:to:subject:sender:dkim-signature:dkim-signature; bh=0yndLeeh7ogCbRBa6xQUCL158NZZ7YW8Ye5mR2J73R0=; b=g4yPJVCAuy4qt83bqqwhgUEBJ8xDByyZKz+fAgmN+vecOU9o9qH3sa6GspWUt9rWmJ jF5AzrSkPV6ITH8guUr65jAFSrt3h4fC9CrwFR3ylmYYDAh3fH/eCChvZW+BMkPX/LG6 +gYVIoX+IBTu8IL9pCU6s1MyoY85O5xnGGSQTIGQXgf5gehorfsQjkXHiMvimtTUDyu7 TZAJeE4yXE6w5r+4iPUaEYRI+cIlnlM95sHsRElLRyiTkh0KSYucsq0jxSrB6+q6+TwV JYAXMiSfFBxw/vz97vEpWnOudoWuUFJEIMjZQ6yYg8ZSh/FBSvw4zfjLJ5vsJ29HpsKD V4ng== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GXtpeChL; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=0yndLeeh7ogCbRBa6xQUCL158NZZ7YW8Ye5mR2J73R0=; b=ibaWb5VkqacqvvHgURZOHJBzO6z0E1ksWEcy7WNUEUfQmKZbkP3TQhRI8Okh8Bv2yb oJ79kK69wLVeqQjd339h1GucoNIrf6fPLv/R6yaficUjc/SrThTLlVHtp5X0MiCrbC2t 1xA4vVi9v5qoQ/T/iWrK4oo9jcpZ7I42f6Ckv9ZhWXpOvSb2t41uKAz0zIk8DLkrtvK/ Gfl8h7YU0IxN0USeyleTVPhSXpx3TF2Up1psd1lbRcDDX8Qlft0Pl649E1zQAnf+hrSp MSE7iSopjJvmYLibD8xxy49V5EkwlLnmVVc2MjHUSfFoKo8a1AlgtqtEkSMtt7prtQKj 13hQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=0yndLeeh7ogCbRBa6xQUCL158NZZ7YW8Ye5mR2J73R0=; b=gUYTkOPNIE8hbd8oXM4QoqKFqEPFVrajZT32Ph+F9Yq3hXMZ+Nn5yekeiIlSoO+Eh9 U7jggWZEObOo8pANIWrxeUaDLCr+qFbjqvGkitlYddP1zVAGa4kraczPJGRPkKnDVcqc NEhZiVl060zE7w3IZvwtNQQ0V1rMJoFI9NqgZz/qCxnSiCleOnlnFyRQ/nrLJxkMV2Na jgwILUWVIaYh+Hk8//HJbsbnRfqH05T1p0h3G+wDFGmg+rNznQlKPoNf6j5HPhxCv9eq zL/9dMdhCcD+pCdyJvPr5afbaWVXUV2GDPA32veIwKd2rygEPT7EN0FWRnDNFWNgGhuB zwWA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:cc:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=0yndLeeh7ogCbRBa6xQUCL158NZZ7YW8Ye5mR2J73R0=; b=HD1KkArMe+5ar5GsbNZfo/D2w6+IACSQT7GsWdibo70aSe6jESxNz6fK0aa4yg3+Lc YBuXiTmxnmHlJBV70x9pVAw3/+xik14Tu0UbVhPzHihCgVptFjHeqk2mLGgawfIoajcZ fJrbtA0rnngKMA2vAgoWEkTsk2rB/geR9sEUChxabysWRDCaPA71kIFzli7zGjdtxMCf OOrmrfm6B9xIf36JHvGJ88mZf9J+1+WuioXi5ln785gFfQLOSXKCLlEm106WZhu4OR/d ppuiS0HSBCXxl32Bko2UCb6KLmnIAdplQlaxjnS7hP9qzbHhNDUwbhvGlGjeaP7Wvp5z 3UzA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532QjB+9+1vm81vGVhwjlPbZpRpzi+DKqLu5+ejJLT6I/EA9J+6W 9+zxwGOfu4rJ4/bj8ztfLDI= X-Google-Smtp-Source: ABdhPJyZ9x0KB8N7hIJck74LLV5dO5b+An6gebcCzGheQSXYiP54gH3BFJb10bYz52jMJwQ81dSpkg== X-Received: by 2002:a05:600c:290a:: with SMTP id i10mr5927300wmd.91.1614897753038; Thu, 04 Mar 2021 14:42:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a7b:cc94:: with SMTP id p20ls3589827wma.0.gmail; Thu, 04 Mar 2021 14:42:32 -0800 (PST) X-Received: by 2002:a7b:c407:: with SMTP id k7mr6113434wmi.136.1614897752112; Thu, 04 Mar 2021 14:42:32 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614897752; cv=none; d=google.com; s=arc-20160816; b=yTqEYXYSJqal6v5ixroIGeoL9rTxCvd4OMd9DnupfzE7KdTjkgZvt6Qba7PgMsgzoh frX/BR/5fvMnCfh8ahfps/5A8LJtrYbRW5NvrcqH5VbC7DM7dpvAqMLoA807O4NPQlb7 jyjU5AejIi3grzuiQkoTl2E6taiIaA82sUigYmDmCGh6VKtu4CkLr8vDhIfRLAj1as2A gf32SKffFc3JN1wKfGnDeB5BRGj8W2yuYMaieFcgrUL9gnjWB/ONqvI9gaJZujb6B+7O jOReZuByervmGz64jMPAOA4RoUNAY5r1ebEe5EJl4I6vIRrnCG+OA3mqR8s2rwFDZfqZ vHeg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject :dkim-signature; bh=r8OFoUpd/acIyQDjBS2gTfzZYegZk68ZvIdQ5qJN2Lc=; b=pDtEJdnSJ0E9IlBRJd0eo8EoMdC9oxWtWeKMREdRWbxM6YZYyffif2AGCnIZr/YNTy S4dWYr9mnl0UHyuqCjLLNoGW1Yqb35uWdQSnHClWVhrmcL7g/PkuprbHDMUdD6iisQQ7 RVXeK+vdm0FZ8c0e2kMY+Bzm/Yd47ajUkVuv0mtJXPcGQ7CWC5RhNbS9ELmPgQW/pJU3 doCau1DeRXuPNy6IEHYEwEl+Kl2dsrpCPwF+oBFH/x2NB4PQYHtQVCYXfmJM+r26ky1L JpuZBemBryHaDex1+NwsWAwWbZDhL7+F/c9r0+99Zi37A1KjHyIGeW18TyOttUOIYSrW YCpw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GXtpeChL; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x336.google.com (mail-wm1-x336.google.com. [2a00:1450:4864:20::336]) by gmr-mx.google.com with ESMTPS id t9si46883wmj.2.2021.03.04.14.42.32 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 14:42:32 -0800 (PST) Received-SPF: pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) client-ip=2a00:1450:4864:20::336; Received: by mail-wm1-x336.google.com with SMTP id h7so21448wmf.3 for ; Thu, 04 Mar 2021 14:42:32 -0800 (PST) X-Received: by 2002:a7b:c407:: with SMTP id k7mr6113413wmi.136.1614897751640; Thu, 04 Mar 2021 14:42:31 -0800 (PST) Received: from [192.168.0.14] (cpc1-king14-2-0-cust212.19-1.cable.virginm.net. [77.101.206.213]) by smtp.gmail.com with ESMTPSA id b17sm1095085wrt.17.2021.03.04.14.42.31 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 14:42:31 -0800 (PST) Subject: Re: [HoTT] two's complement integers To: Michael Shulman , Martin Escardo Cc: "HomotopyTypeTheory@googlegroups.com" References: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> From: Martin Escardo Message-ID: <8f4c4a68-dbe0-055b-3462-3230cd09c86f@gmail.com> Date: Thu, 4 Mar 2021 22:42:30 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8" Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: escardo.martin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GXtpeChL; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , On 04/03/2021 22:05, Michael Shulman wrote: > On Thu, Mar 4, 2021 at 1:11 PM Martin Escardo = wrote: >> I wonder if your definition of the integers with the HIT is isomorphic >> to an inductively defined version without a HIT as above, and this is >> how you proved it to be a set. >=20 > No, I just did an encode-decode. I formalized most of it, up to some > obviously true lemmas about squares and cubes. >=20 > I thought for a little bit about whether there is an equivalent > "lower" inductive version, but nothing immediately occurred to me. Do > you have a suggestion? For example, take =E2=84=A4' =3D =E2=84=95 + =E2=84=95 and define the funct= ions you have in your hit and prove the equations you have in your HIT. Then using the HIT universal property you get a function from your =E2=84= =A4 to this =E2=84=A4', and conversely you define a function from =E2=84=A4' to = =E2=84=A4 "manually". This is what Alex Rice and I did to prove that our =F0=9D=94=B9 and =F0=9D= =94=B9' are equivalent. The cubes don't disappear completely, of course. But there were much fewer cubes than when we tried to prove directly that =F0=9D=94= =B9 is a set, and we gave up because the code was getting too long and unpleasant, with too many cases to check. The indirect version was much shorter and pleasing. Martin --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/8f4c4a68-dbe0-055b-3462-3230cd09c86f%40gmail.com.