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-x53e.google.com (mail-pg1-x53e.google.com [IPv6:2607:f8b0:4864:20::53e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ee1af828 for ; Sat, 10 Aug 2019 09:42:30 +0000 (UTC) Received: by mail-pg1-x53e.google.com with SMTP id l11sf39715077pgc.14 for ; Sat, 10 Aug 2019 02:42:29 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565430148; cv=pass; d=google.com; s=arc-20160816; b=T2fylC/m0c1yNQcLq36W7gecb/Z+4xQIC8B7MhmNenqO39V4Kosr1kEw0FBnD0sDpk UDRaacxiD5j6dvd+wEwFwbvKIe1Yf4szt8QU4g2gO5UEDQuk9xCWV0sVy/e0WEo+3ApC 0aNLVAILzSX9ZGY9puldL0E9Ktlhi/Etr0OmDTCG7DWBnEUAGQSyc6RDcaGLEmZgt7UE zKraiXxn4HWZDi2McDsAPxgGoUW2sjmOuoTwrSTqltnr0goAMv7qZNNN+H0VSzA2aVSu qSanjZAUkAUd4bQLMp/OFEbJ7eGKE1BDwj15CFzM8ZtPcX5vtQyp40eDmLujQgqd2CS4 mkkg== 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=72opj5vvEVxbSBrOPUFMGo3a/ugdLesZDP8e/DnUFG8=; b=K/GE7nuBY0d79L+Uyqk2vUPLDs2tXX3JAM6IIUcSBQVoGigIZcrKTJ2e9IV6YkeM2p uzdjKAFpdi+jtbs4FO1UNUNzEoJfmD/LnMkEK+AxXuO+1MX2cwp4OsBT23cYC/2Ot0mQ B4zizn236u/EXfJOEGZFJIkH+4CKcRl6NcdSwGOS17TBzItrn7NODBFAwM68zeEmghi1 MSYPab3hN4S+ZdOegK0Vwa02gAPchsJ3/sop4JrENiRIGhf4t+r4DVBtMx+YzOB5z0IU agvTN8BR5SLBF8nZmaIG29jZ/TClQvgSeQZ9t5XIw6f8XLDysp44zoCqnaevoSDRNkgn 3uyw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Lx0lfzWP; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=72opj5vvEVxbSBrOPUFMGo3a/ugdLesZDP8e/DnUFG8=; b=L8ndDo63vN9tLsJFYdd0HigVMLtDNXXEp4YuVVwl3EgqWTZsltamZQ/LM77gkcmLV7 OAoaddnO7Gt7johQAnLnhtwxpEFtXo527lS7tTVeorBBqyycus5WcfGDHFdTDFeUwVmh Ndxb+ExnQNAgHd3U2E7Cz+I0JUc8nFlH3XLJ6XYFZwsy5B4OWpqtjh8W7Xjy+gZAMvIO 8uzx2tfHTpy0rklU1sI1bl3DE0kL3QHHZOjrc3QJ0znwuKMtWXFMKaXkAQnV+uRpgq0u UEpi6f7/mD1n+u4ukYgUBpfDuuJsWAM70iH5VFRfkbeGO1BXB1C4Bz15GDQfaC3YGlRJ ym8g== 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=72opj5vvEVxbSBrOPUFMGo3a/ugdLesZDP8e/DnUFG8=; b=JqMsRcDsSgJ3nzQVvR+1NcJXv5jsUE7jqMMjqWCwCSARWgpe1iB2zwgOcPaf+7u0w1 tQh3rxI/TXtH+WnNd4XOcNloN95sRHYKCMg6DHguXDeY8q1lKAjd/1IsM1eSjAqshKlF tjZ5ffDaXA4KMfkmV9YcN2R6I/MwYezTmhcYsMvhFJmwFJuASi+crmjudA8qvNZiHeyF ccL6JX/ruS7kVGlnbEZz0i0MNpVHGYSoWwQLEyfiSgW2GxedE06XMLfL1Hx/xi4aGO2d tiPrYXfLCXws+NRa2PTWL5pXOlG7dAI4FIG207NKh1yLZ2nvdtsHv++S1lRW6lPItpql L8aw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVRuKF+gOW+6VLV+v5Z7Z/dxh3RipK33n0AJb8eTm9TOYbWO3q5 krTnr7fjzpxv6K4P/0Cli/k= X-Google-Smtp-Source: APXvYqwhkpHrvBxCryXB7dkmJIm+PYN0bGAUGE9wBXsA7o+okP0WlmT68Cz99TvFrANoEGSnXL4lHQ== X-Received: by 2002:a63:4a51:: with SMTP id j17mr21306407pgl.284.1565430148288; Sat, 10 Aug 2019 02:42:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:45cd:: with SMTP id m13ls20487781pgr.3.gmail; Sat, 10 Aug 2019 02:42:27 -0700 (PDT) X-Received: by 2002:aa7:9834:: with SMTP id q20mr26630238pfl.196.1565430147873; Sat, 10 Aug 2019 02:42:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565430147; cv=none; d=google.com; s=arc-20160816; b=V6MPvSH/tmmgpOgK1/RjShje8byhqAkICv5Ms70DzV2jMYOndYk40dp+rQ28gdVk29 /VgYl2D+DAw8W9AAPMAqh5CtWeOUu1h9v2HS9TAciBzoSYy7BePPkpCbbkIwGadKNdUu YYxpE+FcFL+HoL6fGOSVRjmV7jhO2WLC8Mk/qXNHDD02yrBdYAc4nYoXSvtSEUlJ1Vpt dop0c6T90jOgs8EBLDI4mp35PE6H6IYmKqe2D8gcSelQOU/3RFSaCuxuWPEFEnjeL1Tt L64jX7QwdBflzpLbwfhVeYYS0L4DR+BzUI0s88jchvk94evT69j8nTifHclTj3WWCsHb Z61A== 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=bfGqOFIjftC5bIQ2E00ZNkpwPfh29jc5n1pZneTtwBU=; b=bQIY1/9IDbSxZZNelSRkXj7in7SQRxupqUuekPkMFjt0YouIBwj4fkZM/tiiqKt23e sAKlLoCo6s3qSFk5sXMP0x/0R8ICLXhGBqjq1aJMDps2ky6mJcwqwTbZqxHV3UMboTMl b/WujVyUc5Gnoo92E0plDtxKaHSf6LID5oJGyuC4hT9WDcLodajBxT0QHu/vn3LqGc1k HjGE3pA1DiXBnc6hozRGq5lozuBkBXK9LSF/OR809k7WG+9YR/FX02XAiVKUCT4KO3ck 1gAVIGcVsShVzGZUjZ1X3oxP5mmafBx4PW77vNLnGIkc6i0pDo96bjBultXmyKwvun/c wPRg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Lx0lfzWP; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb31.google.com (mail-yb1-xb31.google.com. [2607:f8b0:4864:20::b31]) by gmr-mx.google.com with ESMTPS id y13si4004990pfl.3.2019.08.10.02.42.27 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 02:42:27 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) client-ip=2607:f8b0:4864:20::b31; Received: by mail-yb1-xb31.google.com with SMTP id j6so6545168ybm.7 for ; Sat, 10 Aug 2019 02:42:27 -0700 (PDT) X-Received: by 2002:a25:af45:: with SMTP id c5mr17481946ybj.193.1565430146945; Sat, 10 Aug 2019 02:42:26 -0700 (PDT) Received: from mail-yb1-f175.google.com (mail-yb1-f175.google.com. [209.85.219.175]) by smtp.gmail.com with ESMTPSA id q132sm22768737ywb.26.2019.08.10.02.42.25 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 02:42:25 -0700 (PDT) Received: by mail-yb1-f175.google.com with SMTP id t5so3335456ybt.4 for ; Sat, 10 Aug 2019 02:42:25 -0700 (PDT) X-Received: by 2002:a25:9946:: with SMTP id n6mr15982741ybo.25.1565430145195; Sat, 10 Aug 2019 02:42:25 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> In-Reply-To: From: Michael Shulman Date: Sat, 10 Aug 2019 02:42:12 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Valery Isaev Cc: Jon Sterling , "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.20150623.gappssmtp.com header.s=20150623 header.b=Lx0lfzWP; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 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: , There is a bit more subtlety here than is evident from the brief description, since everything has to happen in an arbitrary slice category of the model category. But although the slices of a cartesian model category are not in general again cartesian, they are enriched model categories over the base, and so I think I agree that this works since I lives in the base. However, section 2.2 of https://valis.github.io/doc.pdf also appears to assert that an equivalence can be made into a line in the universe for which coercing along the line is *definitionally* equal to the action of the given equivalence, and such that the line associated to the identity equivalence is definitionally constant. The latter seems like it might be obtainable by a lifting property, but I don't immediately see how to obtain the former in a model category? -- 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/CAOvivQzzLHnq%2BbXBzkFv3tST0GEUo4f2zmdj025LTaq%2BEMB7CQ%40mail.gmail.com.