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.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 23771 invoked from network); 5 Mar 2021 02:27:19 -0000 Received: from mail-wr1-x43b.google.com (2a00:1450:4864:20::43b) by inbox.vuxu.org with ESMTPUTF8; 5 Mar 2021 02:27:19 -0000 Received: by mail-wr1-x43b.google.com with SMTP id v13sf368308wrs.21 for ; Thu, 04 Mar 2021 18:27:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614911237; cv=pass; d=google.com; s=arc-20160816; b=MHBpiEKYTImmuncK+VShiGprXK0s+DBVUKdvTsfRfgovCI3TFvfIciG5nHwJK1BLKM JDGMluc5QZBqS+YqwEyqwG0rFl3C5TATKjd65NQ1X1EZ1+09adfvZlRn7rDqFx3NzIPx YhELDbyFvlOoNW7mgl9lRds27+IvNipjrwvud1PTL/ZVRtA+mPhV/Jp80J5yEseT0g95 hAYYtiSekEPiYOvByx2M/07MZEybFOZwx+0x2GWY+SXp6rddXd0JM/FxP4GHOniMQCRq yxCPtwDQ8aSo86KBCSVbi2H4nN6YYllVva/qY3fzEwNGieBr2vMOGDml9aOXRQesOWQ7 OZfg== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=zLyQrtnXZF4NR8fZw2IkuT9Er81jCX1azuYic5R7E0U=; b=HIp5Xt8aq9YYT6xawU7rcQ2CdYspXnLjz1tDAGaeTmZBO08qgZOD+3n+w8WUqm/h2h uDch2BaDrS0OmFh1WemkAtF9Omt4gzsST2aXWjjn/nZMZg1BXWfZjvz+YIvRi+jD0j2p /rafl32a9TeWXJUKufldxI1lFLXZUh0xmh1M6IDPij0EyOAftQz/LIvm70ipKbBeOVjY 8vvO9s8prmiHPoPZL21AtQmVfOnzizYGPsuA55XkfntN/PoMv0hJ+RewBzHbRHz1tlaN ZCu+O0/434dSknUv7O2QKHRQjtBdiA8FHZgSZLDifM4xUyUsRPYlDt2eyFDX51Ntg/hR 1wiQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=TI3rAlDa; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::630 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=zLyQrtnXZF4NR8fZw2IkuT9Er81jCX1azuYic5R7E0U=; b=pYGRbjd1sxaXWMUkkfNvtVlpDet6p2Es+dXZ7ik4bPt4wB3tvtJ7FYg07umfF9tUpM dr+xgED88ixhegxG1Dvfng5ay2cx1bnj9l6YtTIVn/AGOHnDP6JMf3puzqa0bGgeC6M4 doo2qPCfMpTNXRCoUCkkgT1bXyx4Vq3/CnBXGHORBz4F6zvuNzPpCF4MBUmADhj8sPff IGo4I3fmgQmmvunP4XVfTfyYO/ENAosHgieMzitAVxlh868S8peAee3s7NVcb+Mjik/N U0Viowke/ZV7LBcvWOLnZpoqQDjanownvOXh3CLoe0NeB9cO93FSGGgTrjS/lhvp5BmB mxWA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=zLyQrtnXZF4NR8fZw2IkuT9Er81jCX1azuYic5R7E0U=; b=Wcz5nSGchQrgbCsGHRdAftXVDS0Erfg14rkKo3eUaXDBgNJSa6Y71KfvV/pYgSwqpi jq823JJ5jE4ht6vQvNNw49KkheXT5z8kEhWVRQsT/inAi43xyaqv8qLRdx9jBoZzXDyz EBEQqDCUugCTH3z6BZbZvEnh1JuL7HGDt3vqKGXDXh6a1pptdzO9GZRXtvzboGkBGJ2l kwydRhhhgV2ppAjsKS5jdLHsXbHbP+YztF/L4n+qKyWH1NHz/2KyUt9HhGlVIkPLDcWu zVX9/zW3TgIVmaEqfWsIVbaJxi+X3JS+C+1siUMsOH3p2Ps2s7t9llCPxpgWNzcy3+O9 VHbg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532+pKwhdjpGxtsI57Y8CM3QTvFAJUCXAeIC/GgzseAdCcMkpcYs IxgdbQ0H4i2yr2BBZHQ/yqU= X-Google-Smtp-Source: ABdhPJy0HSiPPmRwiiLa6FOQTLzXBtXwtar8ZaC/X9Wx0y7FbVaAsj1JoseEd41ntFCajheEGXcr8A== X-Received: by 2002:a5d:6312:: with SMTP id i18mr6956553wru.149.1614911236942; Thu, 04 Mar 2021 18:27:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:6a89:: with SMTP id s9ls5692261wru.2.gmail; Thu, 04 Mar 2021 18:27:16 -0800 (PST) X-Received: by 2002:a5d:4905:: with SMTP id x5mr6771744wrq.201.1614911235981; Thu, 04 Mar 2021 18:27:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614911235; cv=none; d=google.com; s=arc-20160816; b=tedcMNgSHkub2puN6jBYIatK0G3TXlLsClPY/ehg6adc031IcQkAuHkSZxG5Z0BWfR umEsPgUf17546TOZ2tl3xZR1hfPtxZGEmxlbOPzEJUyssTrOt1sYKg8/mvQCThi2RKSK WjvRelTy/7kq+LZIol+NRzuFLNz2vEaSBQ3z2e4AjwhmAgbCaABN5fAuVyzRt2viId7q j/LxV7N861mwxZhBqwqjYJnJN27nl5/pMMw9h26HjXH5icSttxG/06MtFj5hMPslxGoa Fvyvo/o+WhU83umcqIAExTuA8T7TTi+6a66UxAdBH87rOa6u4ZfPBZYAKBP0lB+5pbRN HO/A== 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=3RGVOiT/oBGt6DZMwyrQ9IZG27aBABEdcvR2kCGVq/I=; b=G8cnkNFLSUVf1vlnioSiJ1SATwr/a0MWwfoCOSkMTLoWiW53cOq1KOMkJcxXkCzHor Pa0BZev0eLKMESMnfKXpkuVeSr9TNZ+gK+d8dEAEY10XBdPh6lf9kCK5uARxZilf3TOH o86KF1V2EIcBLt5Z2F9n5UDLD7gt4V8oYoBkPXojhfzWK1Jujuc5RRZAV2xbzbXr/mlP CEcfGu0NteGGYHhBoRRZLAHu6M62ZaagvqkhGC/X5nnTIj4S9uodnyG0mwx11ppNbWta bE/vgCi4Wl1tmNwlQWenv+hAQWhpFCqZT3aZL8gOMqqEfEPt+Z+NEyeoFVh4v19kletP Fytw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=TI3rAlDa; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::630 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-ej1-x630.google.com (mail-ej1-x630.google.com. [2a00:1450:4864:20::630]) by gmr-mx.google.com with ESMTPS id y18si38632wrp.3.2021.03.04.18.27.15 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 18:27:15 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::630 as permitted sender) client-ip=2a00:1450:4864:20::630; Received: by mail-ej1-x630.google.com with SMTP id dx17so590088ejb.2 for ; Thu, 04 Mar 2021 18:27:15 -0800 (PST) X-Received: by 2002:a17:907:1b12:: with SMTP id mp18mr416339ejc.128.1614911235574; Thu, 04 Mar 2021 18:27:15 -0800 (PST) Received: from mail-ed1-f54.google.com (mail-ed1-f54.google.com. [209.85.208.54]) by smtp.gmail.com with ESMTPSA id s6sm620390ejx.83.2021.03.04.18.27.14 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 18:27:15 -0800 (PST) Received: by mail-ed1-f54.google.com with SMTP id dm26so510856edb.12 for ; Thu, 04 Mar 2021 18:27:14 -0800 (PST) X-Received: by 2002:a05:6402:c:: with SMTP id d12mr7126520edu.100.1614911234538; Thu, 04 Mar 2021 18:27:14 -0800 (PST) MIME-Version: 1.0 References: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> <58a0a515-d8fa-4eb2-9555-d3a41fdee728@gmail.com> In-Reply-To: <58a0a515-d8fa-4eb2-9555-d3a41fdee728@gmail.com> From: Michael Shulman Date: Thu, 4 Mar 2021 18:27:02 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] two's complement integers To: Nicolai Kraus Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=TI3rAlDa; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::630 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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 Thu, Mar 4, 2021 at 3:16 PM Nicolai Kraus wrot= e: > I'm not sure what the precise thing is that you're looking for because, w= ithout further specification, any standard definition of Z would qualify :-= ) Yes, that seems to be what Martin suggested too with =E2=84=95 + =E2=84=95.= It seemed to me as though the distance between =E2=84=95 + =E2=84=95 and my =E2=84=A4= is greater than the distance between his =F0=9D=94=B9 and =F0=9D=94=B9', but maybe not in a= ny important way. > The HIT is neat, but wouldn't it in practice behave pretty similar to a s= tandard 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 adva= ntage of the HIT - maybe one can avoid case distinctions? Is there a non-HIT binary representation that can be interpreted as two's-complement (thereby avoiding case distinctions on sign)? I haven't been able to figure out a way to do that with mere lists of booleans. --=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/CAOvivQwtAMVnOG7D_A_s1EMAum4fv_x945MLB%2B01Y_pMdEKC2w%40= mail.gmail.com.