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-vs1-xe3a.google.com (mail-vs1-xe3a.google.com [IPv6:2607:f8b0:4864:20::e3a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 68dac1bb for ; Wed, 7 Aug 2019 15:02:14 +0000 (UTC) Received: by mail-vs1-xe3a.google.com with SMTP id h3sf23124479vsr.15 for ; Wed, 07 Aug 2019 08:02:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565190133; cv=pass; d=google.com; s=arc-20160816; b=l8BRWzGzRZANU6OFEE+cOAR9jqXTYSy6p2YNSCDLypLTzOp9Ju36tFcC1I/0oC98ib 83n+n7sd9eBNFPc55zTxD46DGbqe28cwhpgrw0SeHOKIK/42/uM7Wt9x/Is0lMAvFYH7 0SXSyMgGx5SVBq0/7tfNDb5PyzPIST0LW8dY4R76Jhyb/++jshN3owchL5RHstjVfrfE YNi+0fgCLJeQX8N7UBnifd7dLukFv6scMP9REpK/Z2D2RbXtv4VSJuc4usTNQRMRLayk +HlWhUL+jwwsUeMcyfgrAzpMXqQkuRHpJpLWJtPtuwQYzZWs+Yvt59oRoKe6AffARy8d K7dg== 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:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature; bh=NmMeM51dhoCqKwQkjgk+hHiIp80NoWzHk6p595FWL8M=; b=E860uLfII+24HXlGey3GOe+d2XpTrMCCsyae06C79t+MZzhQZUuZo4kjDGfojnVQ9u +gXq2obHYcbniyiPc0YoOQu3g7PhT5pJ201WsoLguh/9Jf9Ba1EzJxy1+kzydqO0i0aa FF2KrGd9m2gLQKFFdrMvYiaenOcCdV3fJlwYx0KyokfZ8KYNM1MaWYtdN5b48Ra3nkJr pr80h00SHkXHQryfNGGfH9rCWckvYiGm7cNL3hfqku159BNpVQKlNqbRuhGhn1s2fO2Z f5OYnx2jC0EnZhoqADdqp05LeTPhPDjiK/yfCP8Q7sfjt0A7cjnT5+wZ8DUJ5r0bTH5x /5Dw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=l8Z8mMB5; spf=neutral (google.com: 2607:f8b0:4864:20::32b is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=NmMeM51dhoCqKwQkjgk+hHiIp80NoWzHk6p595FWL8M=; b=ePhOa9c0gaRc8mq1WzyLAhq0Z7eI0KkGjOcZj+3zzeH46jpM05b24/+e+ocx8C0gWX H7hrbzJ5Z/MkbsICBsV+N9bt7D2SgOimCqFeNJgtPTEXFvqHmSE8uiZsH0D8yX1AsIpU PVP6XKTE77XVVQHKBZyHTfVqd2hNR+bnIPvMC2KpKS43px+rBjH5EueMbxlFenoYdVDB zl5AuAkKbcGJeiEl+/RGlRlUpx2GH6gR0gvfXnfuHz1GxTjm22GobVE8rdXwcKqpcA4q MPLFojr//Ipbv2VRXe/pnHMOGFFEV89HKXu7USlQsuLAeip8ZLc4PbCycXpBpLQU3IGO ZX+Q== 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: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=NmMeM51dhoCqKwQkjgk+hHiIp80NoWzHk6p595FWL8M=; b=jNC1avaq5qM76XX7dDu8KVyd2YwjSn1A+cuJqACX9TiZpwGJWPENM2TQwIekfuyDM8 SXGXpH2OieXHCaDYHvvQZSUxbIPcOUJ3yTSeadLz+cfYB9oK907llKHGXQ5FETKEH5Yo 9akV7WKwXQSBuDmo5uWfD2KogbRaBNrOw4EcL2sOXRRs+kfLESaKiUqJF1jaHxyf2ig9 HIOZ7A03WyICHf8EfFJ+s3Q3ocR9xQYdlZkKJUaPREWWovpSPNX6iqV/ziArB2v9cFW5 +6gK77zZDJ3T0X4bQpZil9Ca5XXMG/NBSACYOvqEh8dCGGT8oo+U0sg0gtUKF7qF3uTp ZzRw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXzG5HEMOND8feIyhipQNdfqsEajQfbJ0BgH1J5A+jPve4oA2Dg ENpg+QrygkNe6KTEYxF/5sk= X-Google-Smtp-Source: APXvYqx8VjiEMVsyaQKVU1CTQP/uO3RauMaXVu60rsqmA27/GmCevEn7bta5dff4sBrIt8tZ67+iJg== X-Received: by 2002:a67:8907:: with SMTP id l7mr6347435vsd.194.1565190133310; Wed, 07 Aug 2019 08:02:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:2a09:: with SMTP id o9ls6611425uar.11.gmail; Wed, 07 Aug 2019 08:02:12 -0700 (PDT) X-Received: by 2002:a9f:31a2:: with SMTP id v31mr6179710uad.15.1565190132880; Wed, 07 Aug 2019 08:02:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565190132; cv=none; d=google.com; s=arc-20160816; b=xl3H8nzL392zp08YEWJsMFakWcOUDeQFpZPCv9lj+t6amZVJaiGLyebaWcq8UjbnU1 vAQwAhi44Y2XutgZBJgR3dGncSG50uUsqaA7qFM2FNusr+T9YCkFxx5RNxoWA0yIxapn RoMX8vr+wk2ysHT4KNyyy4C79rwEpRJlkvgXUEDO/vjyelkshA1SiPqjjEuIoqA2osQp 2youq2uHB+WmKhvGCBdCTyb5m7zSe/2nC7h+rakTAEWc3L0MPtoVH3rt+Ko6OPhzmoEB OvAVSirx+iSCG3URdlhQg6kh6N79b1vxK+dxr2oHWzmvZag3x2z4eKoFkfHZ9+WSeZyZ xjHw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=e0EaxGHfISxPniZdPsm3sgE3fWWhrKfv/uKOcWt27ds=; b=biOWAEh0WENHFb81/C6m6XBxlECV7j5ARcSJCCx+Nd1qmpNgdP9KUhMqMKuFJ2n1Th gCSex6nnAKoe0zJOyGU+NiHi5SUPS/9o7/BvyYAuTjT09Vp1T/xtopGbFKuK+2r8Dhjm EMfeD2V2PbuayuRKaGitH6crSJfMkVHKASLIXMLM8JDqLqpm8uU7zpdEoZl2+He2BIwp nWtvx/n8OLAiY4CGfKqZzMNqcfVZoVqstNZfKM2SqkUZGgLJrtY991PYU7+OXiHgA/ol W7u3r67UF1bCvsTi05P8Z20xSMxIDtkX1j/Olm6hq57Iq44UkdmFJjx/kxKrCd9ERLsz Q5hg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=l8Z8mMB5; spf=neutral (google.com: 2607:f8b0:4864:20::32b is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com Received: from mail-ot1-x32b.google.com (mail-ot1-x32b.google.com. [2607:f8b0:4864:20::32b]) by gmr-mx.google.com with ESMTPS id k125si4807817vkh.4.2019.08.07.08.02.12 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Wed, 07 Aug 2019 08:02:12 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::32b is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) client-ip=2607:f8b0:4864:20::32b; Received: by mail-ot1-x32b.google.com with SMTP id l15so48173468oth.7 for ; Wed, 07 Aug 2019 08:02:12 -0700 (PDT) X-Received: by 2002:a5d:994b:: with SMTP id v11mr9763054ios.165.1565190131436; Wed, 07 Aug 2019 08:02:11 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> In-Reply-To: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> From: Andrej Bauer Date: Wed, 7 Aug 2019 17:01:55 +0200 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: =?UTF-8?B?0JLQsNC70LXRgNC40Lkg0JjRgdCw0LXQsg==?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=l8Z8mMB5; spf=neutral (google.com: 2607:f8b0:4864:20::32b is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.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: , Very impressive indeed! I don't think it's necessary to ask why we need another theorem prover. However, we may reach a point when some consolidation will have to happen, one way or another. Functional programming was a bit like that (slightly before my time), and it consolidated around Haskell and Standard ML. With kind regards, Andrej -- 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/CAB0nkh0UKEgnv85QEFt44CcbA9To3Js%3DEAhdB0xLy0M9F6Z2%2BA%40mail.gmail.com.