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 21285 invoked from network); 4 Mar 2021 21:11:44 -0000 Received: from mail-lf1-x13f.google.com (2a00:1450:4864:20::13f) by inbox.vuxu.org with ESMTPUTF8; 4 Mar 2021 21:11:44 -0000 Received: by mail-lf1-x13f.google.com with SMTP id p12sf10347403lfu.7 for ; Thu, 04 Mar 2021 13:11:44 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614892303; cv=pass; d=google.com; s=arc-20160816; b=vV5hlvFfWv75Atmj7gNWVGd277KM4/YWoy+eOpVC0XsqgdELA/prStt5eyTYrlutF1 +9pbcDeTFt/Ehk0WuklQ1mjxY89h6FmyY5SfQJ6kuXvp9K2pqj1GmndFynQyMYOG+wyL JS2B2gbaRgFrVsVbmkqCn91khPIbqr5CnPC2hHyvbTB3VEQyz0vq3PHFzSQ03KKIVmkf PoNajUGVccyuSNs+PnqKl3D1VMCFVfoaIuPwv3ZKQ3Kh/o4EOzNTMVMLP0MEAUAhV05H IUmG9CA5j8DxSYqa0xvG9lfQWFbhFgG2vgDRutidDGyntAX3zAz4zmx24M43g6jfVn0h +mVw== 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:references:to :subject:from:sender:dkim-signature:dkim-signature; bh=D97ttnAEoNock3Fy+UNeOc7OmabY+UAFiyttmFaZQKY=; b=bNjjWoXjwoyGBly83hpj/PPNfWhskaek+B5rW78XxMwF7/bz7L/91b3qCAJ3fpAXhP ij3A5EeRwfRKqkqgqZ7RfD4wT5Euxc5crQrvaYti5E9c3D7ikfTQKl3Px3rhK7wY3LBA 4ppJ4hFloY+TRlOUEbtgPiMP0gr7a2F2PTW9Bjc8DAddiFAL/Gs7kJYK57vOVFZwzlwL OQRS1JU5okzzkdFfv1fa8VnrF53UJ9EeBLkbhLtq1Y6JPn/qLtGVDoW1FZHzWK1WCYu6 LeiCSJ0TbU2R9b9/NS4lxCgtkM1uNw3aJ93NnjC1L+CynOQfXih+dY0K/osk/+6QHMfq mVYQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u41vbadJ; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 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:from:subject:to:references: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=D97ttnAEoNock3Fy+UNeOc7OmabY+UAFiyttmFaZQKY=; b=RmcMKXXgeetBqUDEBfND2p6bUzZRWNBBRGEhed8MX3+B8yWZhwrV58Mr+DJ9FmIGlv YrKA41Ube1Btysw5wd41JJ+QtdwpVFftnVgTpMadlXryH3X/PD8FvE0YQKFBJziU84zh atL38dHFub2qcoj7ewJyEcQAKJ2oWIkTTBr9yNGHCTBUWWZvUIGAZWdWkdJFQOAqE6Te OM/6JuS+PuhP8s6BAooq2I+RKDk3X/wB2mtw49bDBcZeM7CHhbvGHvkHn6JOPZE8Qxyl fMLPomEe0vZHsYBVpTE4lGq9Bsfm82bh+D1AnlFiNU3rQ0w0LxUVPMdZHe8T9x7qzjD0 Gozw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:references: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=D97ttnAEoNock3Fy+UNeOc7OmabY+UAFiyttmFaZQKY=; b=TuZ1B4rGL7vbiXJzdj/ZHoI1zlar8xk4/9SnGIthw2gXU/jeyDb1dfSQ6G2AjtY4SI mGxQPZIJSAtSL8y3XFqqiXZriwfkXWPlYiJdymZ8NgCOqgKEf1jrMDdVoGbHtcwu4R5i WG907eYbQ7vAnd27RwzT2uNsLwTsFaarwA7n30J4O5luoQxGGHWBQ+dugcm1HC53jOha x1/Qs4fKOPMq9onTXwh3lca3id3O4gGi3U6Ue8nBnpedUzh2Cmxg+h2tzP1UcWRk1zHo mwe/b73hacr0j7P8ISFJGFSyz95ZaztJ4ncdRja7nuqFMLXa7zRdrnoj/8LuGOsajE17 5iPQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:subject:to:references: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=D97ttnAEoNock3Fy+UNeOc7OmabY+UAFiyttmFaZQKY=; b=eNsnE/EMkWzjvnfgJinlvOCFnUDW/I6IB9HVra5PyhPK03GOQ/mmhhzQmxAMb71iJK GG7k+XVEBrgru5f6j5Bp0+nq1rvQ5e6ZR++jVsmhglv2dD031ixp3aj1fjQ0Ih4rlU6O m4cIaLGF20HtjjVnWmIvso+5TxJe39rZtq8n1OF+CnlOmBsQnS+TKu7UVi/wJHdOvowv viLS5N2eKx88Y0SEfPCTK4A4uwWToIToIovm761/CD7mIfXM37MQ2gCjD+TIycv+rNeU FX3W+SvX4M8j6/fRswvgYEuJ3Lz3iNSDUZZY03oZYHK84UjUZ6/CjkyX1qDU3x92ucPI bm6g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530sl49yBH5INuunavR0hYFcF+5AU3quIWEfxfgbr/pp4mB+Dslg C9fMQmJ43JPcyb5uy+jJfTY= X-Google-Smtp-Source: ABdhPJxtMiKnS/ASygRlHZbr7eJIOkZT7uX0ukEW0MD4LgSyZW7v00uKK3fHW0IQMQ8ZhE1MN3QUfA== X-Received: by 2002:a19:c350:: with SMTP id t77mr3315631lff.240.1614892302944; Thu, 04 Mar 2021 13:11:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:a409:: with SMTP id p9ls1433453ljn.0.gmail; Thu, 04 Mar 2021 13:11:41 -0800 (PST) X-Received: by 2002:a2e:7610:: with SMTP id r16mr3329589ljc.472.1614892301657; Thu, 04 Mar 2021 13:11:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614892301; cv=none; d=google.com; s=arc-20160816; b=CJpkxXV5BIDSCUJQaFr1d4bPPdRU10Ibu58hu6sHB/CFJy1eiKe+bFL55njQ4XwRiM gWQpzJPgUYCu0GKY5TNMoNnSbLSwMI4A9JnQ7XZjgc33jSRVCuUfGE2VUSApKulCwXUu lN0nJY5lWMdtu7Y+xvx12tEXP24kcRnJdSqokO8YKO4hzBNRLTtAkb5J35sRelPPJwTe yb5J6ROvtH85Bz0PAjyww1UqOa40rUrMmk/GiTvy4TyVi6moh3mMjER+p12sd8qHoqUi hfPKGBlR8B7F7G1L30xNIBrUj80vMhTQ1X3mB5hWSG9DVZ8fKfhjJAs1AQVQVBqdADOH 2DWw== 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:references:to:subject:from :dkim-signature; bh=vlWCVaQX7YbeXQyUUFERmaKt8Lku5ndTyb53I3VXqzE=; b=xHhf2ocJXfXnKnWAqO64jiEzxO/wLed5NVOwLIvH7p1rtRhJ7B6RP3c19XPiDP4XEk eu6MiJnvdrZyPhYiEQggeyoDSf5i0aDa+VMfmnFbrwaFfWgERWDzd3PjJkX7oIqG6Ggb MMua50vCFzARUHO3PZvXCP50nn1sV7hxMeq57iT4SC7YHFcz70fZTFGjCuuE/LuWGCrA 6my/UQZPPuGPDdiQljq57/CSdxfv3yHf/L/dOqGZvRyWwDTyD7aUyTYgS29yyxMtWsD7 aSrk1cm3qui7CnHdzTttb6/5JwJ/nHPMpBkpP5YVGJCJxSTly2dBWFwIF2zdZHYBultd SbRQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u41vbadJ; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com. [2a00:1450:4864:20::433]) by gmr-mx.google.com with ESMTPS id o10si30184lfg.12.2021.03.04.13.11.41 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 13:11:41 -0800 (PST) Received-SPF: pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 as permitted sender) client-ip=2a00:1450:4864:20::433; Received: by mail-wr1-x433.google.com with SMTP id f12so25407621wrx.8 for ; Thu, 04 Mar 2021 13:11:41 -0800 (PST) X-Received: by 2002:a5d:4903:: with SMTP id x3mr5951972wrq.143.1614892300887; Thu, 04 Mar 2021 13:11:40 -0800 (PST) Received: from [192.168.0.11] (cpc1-king14-2-0-cust212.19-1.cable.virginm.net. [77.101.206.213]) by smtp.gmail.com with ESMTPSA id h22sm999791wmb.36.2021.03.04.13.11.40 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 13:11:40 -0800 (PST) From: Martin Escardo Subject: Re: [HoTT] two's complement integers To: Michael Shulman , "HomotopyTypeTheory@googlegroups.com" References: Message-ID: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> Date: Thu, 4 Mar 2021 21:11:39 +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=u41vbadJ; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 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: , Nice. I haven't seen this. But I have considered two similar things: (1) The natural numbers defined by 0 2x+1 2x+2 This is not a HIT - just a normal inductive types. (2) A HIT for the dyadics numbers D in the interval [0,1] with constructors data =F0=9D=94=B9 : Type=E2=82=80 where L R : =F0=9D=94=B9 -- 0 and 1 l r : =F0=9D=94=B9 =E2=86=92 =F0=9D=94=B9 -- x =E2= =86=A6 x/2 and x =E2=86=A6 (x+1)/2 eqL : L =E2=89=A1 l L -- 0 =3D 0/2 eqM : l R =E2=89=A1 r L -- 1/2 =3D (0+1)/2 eqR : R =E2=89=A1 r R -- 1 =3D (1+1)/2 Then, like your HIT, this is automatically a set without the need of truncation. But I didn't find an simple proof of this. Together with Alex Rice, we proved this by showing it to be equivalent to another type which is easily seen to be a aset: data =F0=9D=94=BB : Type=E2=82=80 where middle : =F0=9D=94=BB left : =F0=9D=94=BB =E2=86=92 =F0=9D=94=BB right : =F0=9D=94=BB =E2=86=92 =F0=9D=94=BB data =F0=9D=94=B9' : Type=E2=82=80 where L' : =F0=9D=94=B9' R' : =F0=9D=94=B9' =CE=B7 : =F0=9D=94=BB =E2=86=92 =F0=9D=94=B9' l' : =F0=9D=94=B9' =E2=86=92 =F0=9D=94=B9' l' L' =3D L' l' R' =3D =CE=B7 middle l' (=CE=B7 x) =3D =CE=B7 (left x) r' : =F0=9D=94=B9' =E2=86=92 =F0=9D=94=B9' r' L' =3D =CE=B7 middle r' R' =3D R' r' (=CE=B7 x) =3D =CE=B7 (right x) eqL' : L' =E2=89=A1 l' L' eqM' : l' R' =E2=89=A1 r' L' eqR' : R' =E2=89=A1 r' R' eqL' =3D refl eqM' =3D refl eqR' =3D refl Then the types =F0=9D=94=B9 and =F0=9D=94=B9' are equivalent, and clearly = =F0=9D=94=B9' is a set because it has decidable equality. Moreover, the "binary systems" (=F0=9D=94=B9,L,R,l,r,eqL,eqM,eqR) and (=F0=9D=94=B9',L',R',l',r',eqL',eqM',eqR') are isomorphic. (And we implemented in this in Cubical Agda.) 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. Martin On 04/03/2021 20:43, Michael Shulman wrote: > Has anyone considered the following HIT definition of the integers? >=20 > data =E2=84=A4 : Type where > zero : =E2=84=A4 -- 0 > negOne : =E2=84=A4 -- -1 > dbl : =E2=84=A4 =E2=86=92 =E2=84=A4 -- n =E2= =86=A6 2n > sucDbl : =E2=84=A4 =E2=86=92 =E2=84=A4 -- n =E2= =86=A6 2n+1 > dblZero : dbl zero =E2=89=A1 zero -- 2=C2=B70 =3D 0 > sucDblNegOne : sucDbl negOne =E2=89=A1 negOne -- 2=C2=B7(-1)+1 =3D -1 >=20 > The idea is that it's an arbitrary-precision version of little-endian > two's-complement, with sucDbl and dbl representing 1 and 0 > respectively, and negOne and zero representing the highest-order sign > bit 1 and 0 respectively. Thus for instance >=20 > sucDbl (dbl (sucDbl (sucDbl zero))) =3D 01101 =3D 13 > dbl (sucDbl (dbl (dbl negOne))) =3D 10010 =3D -14 >=20 > The two path-constructors enable arbitrary expansion of the precision, e.= g. >=20 > 01101 =3D 001101 =3D 0001101 =3D ... > 10010 =3D 110010 =3D 1110010 =3D ... >=20 > This seems like a fairly nice definition: it should already be a set > without any truncation, it's binary rather than unary, and the > arithmetic operations can be defined in the usual digit-by-digit way > without splitting into cases by sign. Mathematically speaking, it > represents integers by their images in the 2-adic integers, with zero > and negOne representing infinite tails of 0s and 1s respectively. (An > arbitrary 2-adic integer, of course, is just a stream of bits.) >=20 > Best, > Mike >=20 --=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/9eefbc82-ba49-b101-433d-c3c1e452ecda%40googlemail.com.