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 27223 invoked from network); 4 Mar 2021 22:05:38 -0000 Received: from mail-lf1-x139.google.com (2a00:1450:4864:20::139) by inbox.vuxu.org with ESMTPUTF8; 4 Mar 2021 22:05:38 -0000 Received: by mail-lf1-x139.google.com with SMTP id g6sf12838lfu.13 for ; Thu, 04 Mar 2021 14:05:38 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614895536; cv=pass; d=google.com; s=arc-20160816; b=jwaVNOW2YFZyuOtt9M0N/L3Jz2D8mS8/wtSRJ/jIHuh3Ucu/GUvuPl6K5FliLKiST9 racCj040CSP9tJE1H/V5yB1IbBLoAtIQPOeHOSt/DXk92tw2bZpiKQvfpfeTRwwI6Ald unBMOLx/SOHQKHShsdg+QitDvFKZ8Hyax+ZdWsc6jmT/hHi0FjcCD4fdLvrTMUSqQdN0 IXtR2q3a33xNCHyMfSA1xifuxDKXWHNrJeZDH9TQnC0/H1UmHOj9bP7wiYSURctqpgwW 8/ZaCRRDmgflQLC5WP9IPtTlJLcgOY1mMxxjk+2fdWTGtTJbTppL/uIoQ8qogU9qOErr UplA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=mnEjoQkjOvU3lEi66Q/jNQgst+VPiCYETsO04XCdEes=; b=09tMJNabNPqXrMffdcSlAqKWf8WyItImDPMS7Q8/TRsOFE6O6o2vb09YfI8pbWPueU nQrPPRIM8Q7eaQVsgUPmJiGN0NXi7KT3ApQycmWEFcYPjpDDZxF69QYN8UveP/A2XaJ2 1XreGtHx+3Z6mPNBZLcZoRJekNtGkFWKtIDsvXwgqqwJaqlopPvpoz2i/hz0fHvTM8cx tOzTzFFQymS/2gB9vhhgNm/3EnaVKXs/7SEJyhS45G7GQ96AGPhyjUipRQ3LrN2ZYcDZ kNRAybhK0XQhkeORxJ05PplXws2S4FZLpbk/a7j5/suDRrh3ECV7C3CDp4C3UJ1fwuR+ H2UQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=gVx4heBk; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62c 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=mnEjoQkjOvU3lEi66Q/jNQgst+VPiCYETsO04XCdEes=; b=kFd+s1bVoJj0EaX+4xCJ9X/ph0Z4/wzEqA0fLmSv4h8JJtCX4/PJ/+zFcrxiextIe3 8F6fR3oOjifi2rT3KxhUZGGkZNENVjzuPz5RrrieHnvcleFcPVlVe5Ug5xrYoV5+NItR nmuYMRZukPFOj0QGNjJPae9ESIwGD1Y+jdb74ceGamZmh+HuKRHzamlf9K628xcRljOe WtJSVibq6rXD3pkYJsKQJTxeiVgKIBWD0Mx7ciZFPxqT3k1rWCQqxiIGj3Da1WwtlYLj HR92LRoLzIWAaYs16fSJVotAsvXe7ye4CQ7YwUmRRjAiuFgDR74HPJ/x6lcqgMngYwO0 kQzQ== 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: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=mnEjoQkjOvU3lEi66Q/jNQgst+VPiCYETsO04XCdEes=; b=fd/m+7rY6u4pumNVfPdEvlQJPEkWzoayorCsO7qSl9YXSXKQFSKA9xIPMK7C4yh/hx e7LSeua4HKoKZbwWt4rzVSYTKUiiEOu5bdWX9FUo4ZyDdHRpMQOMifh+qnYHup7G7ugu zNjb6iQVwaUQ3MACzKB3r4oprOYY9nhudzD/iV6Us1KBeC5r8o0uZvCDQZYbyZAUrHvU ZbR3C0Ld7SGKDjvMSxCOXOl31xmpDqnZdVmatz+izk9husmaxGinlVpNyhVG5rRy6ixd V44Vb2B1YzuNTDGedGfgPm5ec1iOaL+jxeZWIz2TFtFWGHQdKHoJU5V1mUEKhzWBShqJ KemA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533chXmsP2Z388axbdfKcAzQY9kuy+huCUx6i8/UtKO+Yvky4Cjp k+4B39Y0xPhV/6Y9KJ30KPo= X-Google-Smtp-Source: ABdhPJzRGCaQfSmnetQaUCwBaFCuk2k9XTNXemoBncieQ6E6fhqK5iUHMXcr4Qx/O/EUJmNqc7Ucwg== X-Received: by 2002:a05:6512:1156:: with SMTP id m22mr3439050lfg.637.1614895536803; Thu, 04 Mar 2021 14:05:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:6d4:: with SMTP id u20ls2138259lff.1.gmail; Thu, 04 Mar 2021 14:05:35 -0800 (PST) X-Received: by 2002:ac2:4648:: with SMTP id s8mr3483648lfo.621.1614895535543; Thu, 04 Mar 2021 14:05:35 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614895535; cv=none; d=google.com; s=arc-20160816; b=YcsigqIljdbqezcLZErM4AesbnCUMd8E5emmWpONd4B4HjWiTxyht3NykyOvecn+aM EHT0AbYB/E2D4ydF7XRvndtX73XLrHUOrk13VuMI+St08l9eOU0qhjuage1WS7Qfemm+ FMXxIHe4ualXev19hZaB9gNINlJ3YrlRPk7zTkaidzuT7ipj0VmY5c4RKU+2z1NLEQ0W UIPO9L99YemjIE6gsMTOSj6U9XH7PuN8/He4gepfP2v9A4OCPESjQnRURDatWXlSa7ki CN2Y5llmO8zU212I+nSM11ePUHRK9vKcbQgGm8SPw5qzrbQ9Qf/tqdloF8fgskJQY8dI omOg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=difolvlMxDRN/H7ofKTbEUQECVLYUPEbPiSno2gw11A=; b=ESjsH5Snd+CwowRidGd+P/8lxcswxLKFkB8X8e61BHmAoGUo4YC+fqjMhCL7Ezsee2 IYEdBjIY+gECVQIO13JLvwNP/IM06rKbkAdHMHuu8f9eTZl2OjUtZ/0cr0hD9nkMr0ko viB91twtIzh9WblZSl2GCt4P5gg1B7TKtpklOYbsoRMstuz3+15vqFR7eleC87I2Lw+E NOAH8x0cEomdGlmeLrjQBaXlB1dOV4/VCXdR34xntVufSDVaS3Vl4SWBwi3ZhGgSGK3u 0G089OHEyI+FKd1X635TNp9rQRxwBPDMl6Z6SXMELIEQ6tMP9MCOMGjTcNQjV9eq2LnN 12NA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=gVx4heBk; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62c as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-ej1-x62c.google.com (mail-ej1-x62c.google.com. [2a00:1450:4864:20::62c]) by gmr-mx.google.com with ESMTPS id k18si28019lfu.2.2021.03.04.14.05.35 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 14:05:35 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62c as permitted sender) client-ip=2a00:1450:4864:20::62c; Received: by mail-ej1-x62c.google.com with SMTP id lr13so52453442ejb.8 for ; Thu, 04 Mar 2021 14:05:35 -0800 (PST) X-Received: by 2002:a17:906:2ad8:: with SMTP id m24mr6580208eje.512.1614895535011; Thu, 04 Mar 2021 14:05:35 -0800 (PST) Received: from mail-ej1-f51.google.com (mail-ej1-f51.google.com. [209.85.218.51]) by smtp.gmail.com with ESMTPSA id pg2sm358641ejb.49.2021.03.04.14.05.34 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 14:05:34 -0800 (PST) Received: by mail-ej1-f51.google.com with SMTP id bm21so33634787ejb.4 for ; Thu, 04 Mar 2021 14:05:34 -0800 (PST) X-Received: by 2002:a17:906:4e17:: with SMTP id z23mr6569688eju.439.1614895533703; Thu, 04 Mar 2021 14:05:33 -0800 (PST) MIME-Version: 1.0 References: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> In-Reply-To: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> From: Michael Shulman Date: Thu, 4 Mar 2021 14:05:21 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] two's complement integers To: Martin Escardo Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" 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=gVx4heBk; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62c 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 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. No, I just did an encode-decode. I formalized most of it, up to some obviously true lemmas about squares and cubes. 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? -- 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/CAOvivQwsn-MLHzw%3DW5wxZ49Bp%2BHS9nr261YQJLgQ9E60K2Pcmg%40mail.gmail.com.