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-pf1-x43b.google.com (mail-pf1-x43b.google.com [IPv6:2607:f8b0:4864:20::43b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f669b04e for ; Sat, 10 Aug 2019 23:37:23 +0000 (UTC) Received: by mail-pf1-x43b.google.com with SMTP id h27sf63913609pfq.17 for ; Sat, 10 Aug 2019 16:37:23 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565480242; cv=pass; d=google.com; s=arc-20160816; b=sGqu7wAJGP66F+6h3+CJg2zblkCtEmMxleWE5r/wnbmHkKx4duUl6cgJfpEgf2gPKl GqhQiX8ishgWLnY+JJp+ts1bb7PptrRUToGoR/CyFSa/Vf9rQN6wgAcY6YXUDB9xS8sG m4Gf4rNLfw44qzMvsEtk/cxskQxb1w3QbU4AZUbaIOfTjF9R1je2qR6QPt7zX8PpsLYz D0SPE3r3lcvcCVn8CbX2NjHzwQTYdSnTmNSkvi56J8lmF6qWKIdAQRRRE3VY6vGOi3bl lNs+koSLUd/YMnUzDMIBbOXqj/z7zRNvMyr/X62a3Sf9xN/Mx+kDRyrrimQWqE3FpwT2 oJdA== 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=R3LNuaZZFrMbxZ8lws8K28C6bt/UXgmaxFZ3/hqaKs4=; b=YYvBoOVzdQnUMzQasvnQTgIjtMmf+Xcv6OGXZSqJ/Q+HHmcQSWwt0VfqpJhC5Ewmrm fkZ6fFJG2ipccS2+bAJ5bhKpy5ZvEKtaUqXnl1eqjmnWf59bkFWuQAf3Xx6+slUG8k/s KpCzufH5wVD1Lh2v6WuP7MyYgUBwkUvTlKGNNMy6DChcwg/c3tyL4/7MWt1ndcysNDuu 8vGylbXeZ8V2fCilb9YBDwccnHyy6+Csa4Pb/V+UEHyh3d2eQXJtrxeQLApe93l8nYae m4PAHweMoIopMKJjZiKnc9Bm0jHpG20ut5MJZId+aB/NModz6sz6eo1LbNexXp6kMTdE BA+A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=DdJc6iDI; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 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=R3LNuaZZFrMbxZ8lws8K28C6bt/UXgmaxFZ3/hqaKs4=; b=dhvfyU0wf0sggHCx1kGWXgKP1Tkge6CgjIAdkyHGer3bQ02CKEdxH0/fvKifQM1gXr 1+AoTxkiuZFUiwifmiL8JJTwRwlw3Kd8y4mUNpHMCRAPA/d1U3HDViVc8eBrY3R8INaC 3dcDcEg2xNtml8T3F7uXT7j2pVnWDMu3+5cB5rXMKQWc4ZYHFHzJBacPElJx9xwBUHX1 LTdO5LmPNfT6WWOhL8UloJ39kApC+Vsv4Bq1fr1QrSJENXLSQ9124aebSW3WHxj2aIy1 j27dfe5CroXIRsxA0JvRrK+X5rE3ce6v+vBNO1husssyL/DTnLaL6xzm81PbvE/Yn0B3 QM+g== 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=R3LNuaZZFrMbxZ8lws8K28C6bt/UXgmaxFZ3/hqaKs4=; b=ED+k49DggNdqqaHU3DcP1MayyD0pb8CF/pRbynWfbJIdsfCzAWTF2KBDzYMhUSXHws exBWkhpXRme1OU+Jx7NIvf8vbnXpMxquAa12389khh3ZsojL57zeXhqXDOd5D6LbQxw8 pjMmbxB0YmXxIPa4/Z7s1vMeETo52ihpcxqXeXK3JvqW6QdM+yTGQSLCinRJEicXYf1p RqNY8vLi2C0/t1iUBG8hZZ3N4eomhCpo6E374Ei7c7l0YakN125kOJL3+UB0Mrf1LMWQ Y5KmVvkbTyWZ/wx/gK54HJxCWhGlj7KoEO5dxGoUCZNu6c2zC1/yyMUBmSDV7jR63CH7 ATNg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVJouJQ5B4Y4D1E+VAFpjyk97BCGhw6yW1RksqR/cJ4Ij3G6xk9 4Fuwti2nCq537BLa3+iECDc= X-Google-Smtp-Source: APXvYqyBykpvu/ABxlyKsjK/y0oCLDAzK91PorzDri1k5AF/qXhGy9c1WF/3rgsi0SGkzZw5DKLjRQ== X-Received: by 2002:a63:704:: with SMTP id 4mr23857883pgh.242.1565480241958; Sat, 10 Aug 2019 16:37:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:568d:: with SMTP id v13ls21773755pgs.4.gmail; Sat, 10 Aug 2019 16:37:21 -0700 (PDT) X-Received: by 2002:aa7:8b10:: with SMTP id f16mr29477141pfd.44.1565480241624; Sat, 10 Aug 2019 16:37:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565480241; cv=none; d=google.com; s=arc-20160816; b=KIbyPKVmKAV4zjjwhNctvBWqo/Ov3G6h3WYyyj7YTbVyaBIHh7aVGKtnrVtPeGfwhJ UE7bd3zprqImUn3MBzfDihBOSaQaXnCG5M0GGAe0bYcVmnD1owniFDgfqmJX89QU2bdf 4VW9Bgu72mhDQvMBaTTs/yGlvtSgFYKWLK18yAtd6vkfaNeCr0rEfU01SCHS6S9PEnN6 9k40iQRX7b99OojULGed5HmroOTdBtOKOkmvJLLu4bvbpF2pHiPiV5fEtPd+76k1Kbml knx87Olkn3QEipCLAxvL+IlWTUlHzmQS+gvriwmXhOcqzE7d8CozRcSugKtJ5rlrGDD7 rYAw== 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=bItDYq7LWeIL8gCfDVU1b9E+4u0N1FCsotKZmiuD9Lw=; b=V+/iTsGis4ps5nKD/R0erp0ENWRURhOdmCBCIOfn6gI7VactlB1KpRlHBTW8HUXRB8 ptCkWLR5imE61nVXWDosrY08JognbFoWkigYM/nXzMM2BHyzv+MTU22CusGH+zUaxv3D 6LU7i/408ZXrVXVE4sN0e6Ru1oH3oj2srnDDvvsiLoz5fK8bcSoEDTSLmseKtdb0raVH EgsQXCKFXfYJ0LhkBrZqSGDiNPcbuIJe7LBpcp+ZJB+Y8b8prsps8qXqv3X316Pwcz7l xceDwBT6r6tW23pMbS7DJpSJzPeAbgMGGxECP/sNChKiIfROd0XREq35g12heNHKt7al ld4Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=DdJc6iDI; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb36.google.com (mail-yb1-xb36.google.com. [2607:f8b0:4864:20::b36]) by gmr-mx.google.com with ESMTPS id r202si258881pfc.0.2019.08.10.16.37.21 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 16:37:21 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) client-ip=2607:f8b0:4864:20::b36; Received: by mail-yb1-xb36.google.com with SMTP id j199so37428600ybg.5 for ; Sat, 10 Aug 2019 16:37:21 -0700 (PDT) X-Received: by 2002:a5b:5c5:: with SMTP id w5mr20110296ybp.93.1565480240743; Sat, 10 Aug 2019 16:37:20 -0700 (PDT) Received: from mail-yb1-f172.google.com (mail-yb1-f172.google.com. [209.85.219.172]) by smtp.gmail.com with ESMTPSA id j82sm22883884ywj.1.2019.08.10.16.37.19 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 16:37:19 -0700 (PDT) Received: by mail-yb1-f172.google.com with SMTP id c9so9936348ybq.2 for ; Sat, 10 Aug 2019 16:37:19 -0700 (PDT) X-Received: by 2002:a25:a265:: with SMTP id b92mr19518368ybi.273.1565480239347; Sat, 10 Aug 2019 16:37:19 -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 16:37:07 -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" 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=DdJc6iDI; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 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 Sat, Aug 10, 2019 at 5:25 AM Valery Isaev wrote= : > The document is slightly outdated. We do not have the rule iso A B (=CE= =BBx =E2=87=92 x) (=CE=BBx =E2=87=92 x) idp idp i =E2=87=92=CE=B2 A in the = actual implementation since univalence is true even without it. This rule h= as another problem. It seems that the theory as presented in the document i= ntroduces a quasi-equivalence between A =3D B and Equiv A B, which means th= at there are some true statements which are not provable in it. I don't understand. By "quasi-equivalence" do you mean an incoherent equivalence (what the book calls a map with a quasi-inverse)? If so, then every quasi-equivalence can of course be promoted to a strong equivalence. However, as I said, I'm more worried about the fourth rule coe_{=CE=BB k = =E2=87=92 iso A B f g p q k} a right =E2=87=92=CE=B2 f a. That's the one that I have= trouble seeing how to interpret in a model category. Can you say anything about that? > If you can prove that some \data or \record satisfies isSet (or, more gen= erally, that it is an n-type), then you can put this proof in \use \level f= unction corresponding to this definition and it will be put in the correspo= nding universe. What does it mean for it to be "put in" the corresponding universe? The documentation for \use \level makes it sound as though the definition *itself*, rather than something equivalent to it, ends up in the corresponding universe. How is the equivalence between A and F(A,p) accessed inside the proof assistant? --=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/CAOvivQxKMPvpm9Vwkt4ARR7R5qLmzJMUkFCrf%3DrFUL5sd4nXLQ%40= mail.gmail.com.