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,HTML_MESSAGE,MAILING_LIST_MULTI, NICE_REPLY_A,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 3045 invoked from network); 4 Mar 2021 23:16:37 -0000 Received: from mail-ej1-x637.google.com (2a00:1450:4864:20::637) by inbox.vuxu.org with ESMTPUTF8; 4 Mar 2021 23:16:37 -0000 Received: by mail-ej1-x637.google.com with SMTP id mj6sf53752ejb.11 for ; Thu, 04 Mar 2021 15:16:37 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614899793; cv=pass; d=google.com; s=arc-20160816; b=0QEzK93A8XnfVahawXrxiUhi9U5TDFyWUwUfA6u/k4G/v/XEtdDGGIwkAcrsi0EXoM wWv8/amQg3RjUanslYpfFgIo+ugWWEn6VGqLrjv7gmYmDDIU1DtUbrck6M7GxLLgcJjS kVmHRhzG7niq7Y5aNoDS0nGSFgGxSg1zKX6U4dbZkhybzTatU/RCtEvuWebdZzmq+Cu5 qjkBwuzOmljheeqB1nJS6oRfGtoxdfpwDTWB7i3NW2Vx5+pVkAgBbLi+JXXCXwps9tYu s7sc2FnNjPZldrycC+5e/WKiPLDlpRVa11u3BvonwBbiTB/+2eDSzuGJrb5CmgygFpsE RWlQ== 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-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature:dkim-signature; bh=EmBAKgn+QNtW6BHPT6+C2+XjeCrYQ9F3tACmO0UkZ7Q=; b=URjxpChPP2jGGLmbUP7EN7Rd1Y9bcL5ovOEwAtz0krC/krNK0fNfmMG4KkQG2cXJqK Yiqp5o0fkEg9GUMy8JkMcFSnQRgKOrJjGlxhK5s6BhjNiG2dZ5HqOHqnMljAVw+OWWzO Vz+Eep4pYWu+qSpMfqIUM6OdTCa3lGb+ensnQYUD4S4x9xeaUa2Ne3InjukYa/wHzg9k cmVWPcNGdsCsbxcTR/ZLeZAsTcP8NdSgc3waMYzFffE3pPnCFCMhCr7SLf5NlChuqQpY oDe+T7fWOtkbjpRsymK55SQzDPeZ82t3MRAM2YOOrpSN+qwBHUO5tEPRTYWssJ9xEOmW WmMw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=YmjIEU3l; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=nicolai.kraus@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:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=EmBAKgn+QNtW6BHPT6+C2+XjeCrYQ9F3tACmO0UkZ7Q=; b=jUXRUA+hHcenqn2+bcK1iiWZHMgI5PVtqSP2yQo2yeNoXUWrdKbXz9oonntX3J5qge 33LI3NOAaAD+wvbepD+Y3Dwrc6QBy8+Ls0xg46w7mT4m4uRg/n4oaCrf1T2DXuxeflRj T8X1EeDftnV5v3SrADUpAIFikxNps4XMVhaA/J71hu9SKE/qJ9vuDWwYqPDrE7W0Vb+m ja68wF75If/pTwfKq9Sj1BlclKPBrHpOkZf2ThmGbkHHmZQbGcr8a5fuAIeYIdkmx/2A c4Ix1eXEHHtDKthmNbXasBBgAPNcvNxIgPn9C760dhU1tEgdMTHHVouws/XksD/Zq4WS uqDg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=EmBAKgn+QNtW6BHPT6+C2+XjeCrYQ9F3tACmO0UkZ7Q=; b=cnocP9CEHmzrBHkZCasKHJB6Hj+uo87OsKfTLtx5u+YhZFrHMQYwrMkZmgvNNtgkUT JPen8xEXypxZYNSwZFHRp4QBjU1H81E2euc3GAQeNayZ2uyBegWsrNGkV2q0EfWfWHoV lFs42DEzcyKU8jfyVhMCCrRa/Bdx483GFkjcgASLBXdsD98mkWXKzqMu0PU2SlkZzoFl 8nwo3GcnYoXmZRk9UoZ7MJVdjicT5TGqdXigUD/aIk04stpTznpkYGVGf9+SGdIYCOqa M/JCxAq2lOop63qPVUDbX/1p0xs3w7Ykj/ZtUxY9LNvkFoADrIOQ7C3Tg7RtjM59N90z Z+TQ== 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:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=EmBAKgn+QNtW6BHPT6+C2+XjeCrYQ9F3tACmO0UkZ7Q=; b=NmTMkD03P3ruVQGnAs+FEZE09jR8jY6OSXB9p/NXq9/HZ0/CJ5W2qmNMAfFI3vyL6W dS/oKiS3Mxasl4exxdgW8Jq5hsE8Oy25dmOVeaPuuES6oBOh5G+8PsamA79azcdktsgl CpT2uB0UNYp7FQ/l4jDzpPxj237r2XAcUQjP7Xm9aOC0INk5Gw/GCn/CiIMX3uA0gaSE UdNirGqTE6704ioUK5iGyK+rti4OU84K1ySsz+FeigeYi/2/sBu5Zzoatm5xJbRj2IYB YLesi68HYjrt5otx6D5IADOTb/1sOQQ/q7z419PeLViTlmO6OuU4mTyxsfO11qZkrgCu lYhw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531g8nDFsrFCL1kYpd+2q2oWJlVPxKCSEvtVWfuxm3XajfT55XHX 0lAYhoD1LOIDX7w7fuHGA3Q= X-Google-Smtp-Source: ABdhPJw7Ev+yQruVIGSA16eD/kFXYqyNHKPQsHAtwgmZG8y+mAtY0Dn2YBRxjCI7xDWpWqNa4W0bgA== X-Received: by 2002:a17:906:110d:: with SMTP id h13mr6785931eja.357.1614899793613; Thu, 04 Mar 2021 15:16:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:16d7:: with SMTP id t23ls3684455ejd.7.gmail; Thu, 04 Mar 2021 15:16:32 -0800 (PST) X-Received: by 2002:a17:906:4410:: with SMTP id x16mr6705400ejo.446.1614899792533; Thu, 04 Mar 2021 15:16:32 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614899792; cv=none; d=google.com; s=arc-20160816; b=0d2O2t62F0B4mNZvDIo7Wz7X0VS1QkIvQ7wro3+8jzdkRcGI7UyI4HdN4yXdU4mLQG eFrurS9WZRKp5qPqOgxhC3zZ0mfiF65OysSolmR4TZFYJrQNdFL9ln7eRBh2nbsoSnUr 8d6EJKx3SgvmHU6wFOzsA78eoMQEtSNJOUQs6/yXBQ2HMzLeQpcvDIL9EsDM5WpGT6ke hktwLUyvdKs/Egz+G/M+Gu++8b+BWloaMValreqo93Rf47Peq/9p/wn43+CCvXfdLckh dEF+1BnIaeIxd6VeWtKsDSqeEwRPt3lRcrwFHP4biqeh4r1HYxrHRzIh0KVEW6e0AcLB GhLg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature; bh=mP8l8s+feYGUpZWoiZnb2zZEmuuGtv3282CIckI24cs=; b=KmhufWRwqCSbwVWyErn6K3i4iYYDFgfYf6rzMCKw9jmGmZNULAHxBwXjnHZ5/42zSO A3P3+Wb5f+uNXVzI4URi4cYnp/mItj/u49dyY86L6G6zDnkDC3/IKkrSlFX423xGCzYj KoQst4/5kjKtVxmK8eODM3MD+HwfVUnIVwI8UVxmJD+v907sjkO4NmB/3zOkAA/U1u74 bZWO6S4nTxBUhlwRqRjquaiygWjKlv5gDTtqqE+GTSyX3RmtV8YZ2ZsZIuqEro2r7zjh lEnDHEcorU7D38hgQUhmLdtQbaLKCDZYFqF2SWetnbTxKX9bPp04GzXh1WU+Xefh+9X0 JqZg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=YmjIEU3l; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x335.google.com (mail-wm1-x335.google.com. [2a00:1450:4864:20::335]) by gmr-mx.google.com with ESMTPS id jz19si47459ejb.0.2021.03.04.15.16.32 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 15:16:32 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) client-ip=2a00:1450:4864:20::335; Received: by mail-wm1-x335.google.com with SMTP id l22so75720wme.1 for ; Thu, 04 Mar 2021 15:16:32 -0800 (PST) X-Received: by 2002:a1c:9854:: with SMTP id a81mr5793902wme.19.1614899792057; Thu, 04 Mar 2021 15:16:32 -0800 (PST) Received: from [192.168.1.65] ([195.213.27.56]) by smtp.gmail.com with ESMTPSA id l15sm1315387wme.43.2021.03.04.15.16.31 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 15:16:31 -0800 (PST) Subject: Re: [HoTT] two's complement integers To: HomotopyTypeTheory@googlegroups.com References: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> From: Nicolai Kraus Message-ID: <58a0a515-d8fa-4eb2-9555-d3a41fdee728@gmail.com> Date: Thu, 4 Mar 2021 23:16:30 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------342848DF0F062B3FB1379AE9" Content-Language: en-US X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=YmjIEU3l; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=nicolai.kraus@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: , This is a multi-part message in MIME format. --------------342848DF0F062B3FB1379AE9 Content-Type: text/plain; charset="UTF-8"; format=flowed On 04/03/2021 22:05, Michael Shulman wrote: > 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? I'm not sure what the precise thing is that you're looking for because, without further specification, any standard definition of Z would qualify :-) The HIT is neat, but wouldn't it in practice behave pretty similar to a standard representation via binary lists? E.g. something like Unit + Bool * List(Bool), where inl(*) is zero, the first Bool is the sign, and you add a 1 in front of the list in order to get a positive integer. What's the advantage of the HIT - maybe one can avoid case distinctions? Nicolai -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/58a0a515-d8fa-4eb2-9555-d3a41fdee728%40gmail.com. --------------342848DF0F062B3FB1379AE9 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On 04/03/2021 22:05, Michael Shulman wrote:
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?

I'm not sure what the precise thing is that you're looking for because, without further specification, any standard definition of Z would qualify :-)
The HIT is neat, but wouldn't it in practice behave pretty similar to a standard representation via binary lists? E.g. something like Unit + Bool * List(Bool), where inl(*) is zero, the first Bool is the sign, and you add a 1 in front of the list in order to get a positive integer. What's the advantage of the HIT - maybe one can avoid case distinctions?
Nicolai

--
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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/58a0a515-d8fa-4eb2-9555-d3a41fdee728%40gmail.com.=
--------------342848DF0F062B3FB1379AE9--