From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x53b.google.com (mail-pg1-x53b.google.com [IPv6:2607:f8b0:4864:20::53b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4136d2f2 for ; Sat, 10 Aug 2019 09:47:45 +0000 (UTC) Received: by mail-pg1-x53b.google.com with SMTP id b18sf61146687pgg.8 for ; Sat, 10 Aug 2019 02:47:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565430464; cv=pass; d=google.com; s=arc-20160816; b=HfsSPQvnNJsGb+spPhc3oyjM0FUglj35lTP7Wb2ucOWxmZTMXY4eTAglH9H9E4YXJx g9SeUUo+3aOmZjNMdGDQXxFvmfMgFjyJOwWUNlzNjaSG8QEQHWSfoUELxT11H1HeoEKC b/xEwXkcj4UH6EdaQhm6e1iyQ6BdxfrYoRTCPVlbX3tz7dl7vnKI4hmCx8zbScfvVMvM inWzunhqGiMckG1rPHAWf+oBLcdJSmTsosZ6Pxc/dEkMqpmdD0lSPZLPho+xVStzEN4A bUjb2PNmho8ZjF2mDh8Mz0hs0mFnRvodrP2F3lmE2P+rPczcELaKvK5lkYjS4912J4dx +8HQ== 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=q0hxDE8yXMvjB99VKyxXLOsDyCHA2FR/d7Nn3s0Z3wI=; b=IiEcuRlavy8FZ79crdUmL6QrECEbYe2Amzl4hL/0QgFaGpuzlW9jGcb5e1hi4mZTBj xkxe/RDEAttqBQzgwm9TQtVyREgzbj6iyhER3y3JidWTDKpCdNaAXrkFPtKJqZtWZoA4 U0U2HKMcKin3nUTF/4M8M7vJ5uTI1a822pViNSWRTvHXaSrwVmpc/x35CHViXD1VUm6q krsCl4qTRFtUSjgOGES0KNgzbWUE++55E7OGh8apOfGtVV6nOCW+bO0Y+0tMa7aMmpaf RwAmDFhMpzkWQWi5LpEMpq7xkjwD+Y7Gc7+elgyshTTt1i0ksY9/Ey0UoGCjKRcfs11X yG2Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=PZdYqXVK; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@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=q0hxDE8yXMvjB99VKyxXLOsDyCHA2FR/d7Nn3s0Z3wI=; b=NAjfgM3o9iNjWd+9zFIFwyA6GxDYUbRDhJnUvObfU8ohcY/8af1r36QhpBobXiik+I 0Jig/x8dirHsJL3CVYL3BnUGxTv0+qrnKtR8jcQrkuTOt28oZ6Wm3Pf7vLQ/fKtWba/9 CU3mHbJz0xTF0roUASMWqxKwe9Mt7SKukW+CIdmljiMrVPpc3vtclYJkMAsIe5uqMsbJ Js35wTQvHcoe5X4GqgaYJoZw6Xi1UgkEOMqyBUrwfxtHs+ZsWuRc31l3mSQX9B4Yyxzv 9/EeMYgRu3S/DayePeoiF02GBOjihjmWgqHW41AVOi/Skj8Db5Upu0yuDq2OPfezr95x QhfA== 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=q0hxDE8yXMvjB99VKyxXLOsDyCHA2FR/d7Nn3s0Z3wI=; b=Tl/Yicvp00LHyC+NUyudpY3s9FohxBNYv/RsO2G7b3ASJLxScA8UYLFqDoTvjrJRMk hbfb1FjYKJhR0KEWNDEWG4CdTvTyCLpAtmt6I/glyLBXsE9yBCFPMtuJlBbcaKm81UX0 OCbNcM8kicVeCrESLCRp6CfaqqxSCuL7RyyiqNP57RDGWJCxC6RXURk0QPQOhFjh9Sku u5H1lSQ35bi0VejSko+a3umfvTv5iYic4cvWHTAUtZgfye60GHOzg5Y8VHTbLYtTKANI Sq4o0xM+oW8h7iL3CrmPHFjJRR+OYS+xlDMI33omChTwFfW3TFU6HkXEf5Morwrt1zDd z5dg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX8USOfN55t0orgIEZTzIlRLeIRlZZvtsFlvLv/phhTBUuOUWfK 1bpSJKYiGJNbpg0s9jV2j5U= X-Google-Smtp-Source: APXvYqzRRY1+9iWPq4v3z7/PR7W1Lab9xmmWojuKw9wdjpktsoQF3hRnRXxa5nlSOsj2WbqkN+9l/g== X-Received: by 2002:a17:902:343:: with SMTP id 61mr8736871pld.215.1565430464168; Sat, 10 Aug 2019 02:47:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:8996:: with SMTP id v22ls541086pjn.0.gmail; Sat, 10 Aug 2019 02:47:43 -0700 (PDT) X-Received: by 2002:a17:902:9688:: with SMTP id n8mr22785275plp.227.1565430463814; Sat, 10 Aug 2019 02:47:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565430463; cv=none; d=google.com; s=arc-20160816; b=B6ydB7BONiWlg84zmrZ5So07L1zAmuQaCCJgl5f7j9h1bGYYtvsWSxwe4gUD54kAn8 V9QsXnGLgW6X7XQd9Dkf2mNFl7KKQXv/DEhC6O2Gx4wyunJdiMexjOn5wEoZX995qnMR 6zhXroi1NmZgrRVsHQZ/Mo0z4zjUqB0nJv9yGoJlwQ8RWP3Uq0+E2jeYcG1W8/UD91r/ wf7AVW73O29qLgD/lNsXVMiMcd+mztAgLAmZcu8tGe/0EV7SUtJL+SvhlXepclMhvbwg X2BQ65g4OpwHaLn9TmydH1l6jm3+Hl2IC5ZaRNfsHMteVb3zyn9qqirzw4i6Cb1xLGm+ jltw== 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=+vIiSc8SnI1dnhaWxe4zmPJX8AM8x234iwlTMCtMRQk=; b=Iu3aRGxKIlOrnowjRZ+UqOtqkaWzQ6USEULmDegVlfOog7/LJkGlyeU4SyhYT02kg0 RenA6V2iTmTzE5W8NSaBN3ZyeXnQbH15CE6VfKM1XN3r5GMJo+mxuQM/8JPWKia6sYR6 76sx9yajUF02PIwVOf5+SBYtqtYSegXMh2X+HqOCWAj35OEDQPuqYDWs+mS/rIib6Byy qoKkB+nCDNBg0MzxHohH9esK/OKHW6/KjVPehaku0wW0bhJderGfKHx69rUwFELqSl1H it+KnyOlDfNVjZULSQ59pSxIy3JS5kofKykQEoqWJv5DJqKzo3AqHRz1ytLN3ZaWRe8z n+cg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=PZdYqXVK; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id d9si82816plj.5.2019.08.10.02.47.43 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 02:47:43 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id w196so8820926ybe.13 for ; Sat, 10 Aug 2019 02:47:43 -0700 (PDT) X-Received: by 2002:a25:810d:: with SMTP id o13mr17725953ybk.422.1565430462904; Sat, 10 Aug 2019 02:47:42 -0700 (PDT) Received: from mail-yw1-f48.google.com (mail-yw1-f48.google.com. [209.85.161.48]) by smtp.gmail.com with ESMTPSA id f129sm875427ywe.30.2019.08.10.02.47.42 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 02:47:42 -0700 (PDT) Received: by mail-yw1-f48.google.com with SMTP id i18so1544963ywa.3 for ; Sat, 10 Aug 2019 02:47:42 -0700 (PDT) X-Received: by 2002:a81:9205:: with SMTP id j5mr16096622ywg.477.1565430462192; Sat, 10 Aug 2019 02:47:42 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Sat, 10 Aug 2019 02:47:30 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Valery Isaev Cc: Nicolai Kraus , Homotopy Type Theory 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.20150623.gappssmtp.com header.s=20150623 header.b=PZdYqXVK; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@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, Aug 8, 2019 at 2:56 AM Valery Isaev wrote: > You can say that they are hidden in the background, but I prefer to think= about this in a different way. I think about \Set0 as a strict subtype of = \Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) is only homot= opically embeds into \Type0. It is equivalent to \Set0, but not isomorphic = to it. In particular, this means that every type in \Set0 satisfies isSet a= nd every type in \Type0 which satisfies isSet is equivalent to some type in= \Set0, but not necessarily belongs to \Set0 itself. So, if we have (1), we= also have (2) and we do not have (3). It may be true that A is a 2-type, w= hich means that there is a type A' : \2-Type 1 equivalent to A, but A itsel= f does not belong to \2-Type 1. How do you ensure that "every type in \Type0 which satisfies isSet is equivalent to some type in \Set0"? Is it just an axiom? Also, since \Prop "has no predicative level", does this property applied to \Prop imply that propositional resizing holds? --=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/CAOvivQzAdt3Pj0TtoxZA29R9XyZm%2Bxwz8-9AN5ap0iatf-%3DFLQ%= 40mail.gmail.com.