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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e52140f3 for ; Thu, 8 Aug 2019 12:29:37 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id b4sf61437773otf.15 for ; Thu, 08 Aug 2019 05:29:36 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565267376; cv=pass; d=google.com; s=arc-20160816; b=tug1Wr1MuYtcAkOkBj2F0JIOwV6yhYUTVxKrSde22nTMQWpvcTkyH/eA20ClkdbE6a 25lfomU0mCpBd22PqaE7cub1kBX8Rwwbt0qOIZBz5resD/PzA7iDctJ4d93g1oWm0a/8 kkm2oZeg9YmiE2rpXM+WOKj6eBOA6C3ntTdEJKnITcmmc3SCZoUCnJ9rvI6Tv0zs+cjn KH2z/lGc4s4/8ST0wAKlMeQ4fJKy4mYxBVsbk3GIsbpXvwYSD9Ucn9t1WG7H1MRnlsHI 4WQcasB3vTLxX3TPhWuNToGql8yp3IWmmlEq6QfL7BMxHj2ECBSBab8bvEqO9e4Vgtl6 t0WA== 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:dkim-signature; bh=J6exGcMaOCn8T+/nJRud9XKUuc9O0hVtk5ZDoZrL/lg=; b=FPlBysyoSh0CmSIYpoqusMsFMpLBcOSMAHVEurubZJ2i6oERplNq0PgyrqQtvB78dj zTbBZPUnterCgObNBXl35pXOFfGHygr9h4qwmTB26QPWv+6quylBIdouwA+fqxYnwNLc or6fLqTiSQcqIrFIFd2Mf8dZl96RDc70+ax6vKk2Z7K7LAXiZdiIt3W7kyxWs1fyX+nb ZRw7CY6SQOMgXNN0faZ8LG1Kmvxbrf3F7xw/9JOwB3dq5n9MqvTi/xNfsNZOPmQXgBnL YCaxFO6E0N60ZGo3Bduwpk/3iNRy3D38PSJ0DQJVy3NqwBTehfNwmIP2tVpJN7rKMZfN U3hQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VaEN5CH1; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: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=J6exGcMaOCn8T+/nJRud9XKUuc9O0hVtk5ZDoZrL/lg=; b=G4D60uzGKSljMXbmtKTw83YYKjmxTl85aEv3Lf7iTYAiig5sZV6RLxbV/7ZtXwYWwF KzZU1Ea44CSXnHdr1Y1qEZkwz+q1D69JypqwnQZ5dh74h28e1w2X3Qtai5MO+c/V9UZK iQ96LryCP4utTexoKiiFAPA4qZdyA1U/UXix3QOUeQJA9ltqyJDxqwNS3nRu3en/oWka LEsj2JZk11MfPvgr+o9oizFqywJfTXHUcuOSvsFMY/SfUIfhFoZ/58+oB8F0y4FtooRL S+7RnsPnZHE2D4hGwzPMafHFqEkBH3W8mBqa1e4WdZWmcctHHuD81w6Ew7S7FfGoXA10 iv1w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=J6exGcMaOCn8T+/nJRud9XKUuc9O0hVtk5ZDoZrL/lg=; b=K6M9SSPI1AvgUuVyhchM84ZGILNX0s/zIGKE1CefUEMChfXEKyskVcfsH30OhpAQN5 pW6UoUBp2virM+3BmVpPKNxdAc8paSACOLDkR/0autfIwSFBjbdc3Owg2FA0sWz+Cpkj QExQFO0Sj0xLPMWSgC80fwCbZIFlF1bbxnoSELFLv77QEGpZI14EH6oBgHDa7x/LZHM8 OSfSyEwl7e2lFj1xVYRM0W4eV1PsXmGLMFR0p0G7D9+eaYAO1AwPrq8xi+a2OQjT4alt xa165cfGQ9bk9bBnQ75YzmCm64sfBUAXbgomIE0zM2+hVBw2p1ZpgL1wLP5vveyB3uWQ KrOg== 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=J6exGcMaOCn8T+/nJRud9XKUuc9O0hVtk5ZDoZrL/lg=; b=hx+TcAO4EOupLYvqXKRQwV2DF3WPyZgOJMCs0tx2b7+SZlu6E+CH0XeU6UfKbTNiXs 8ri3mOBBo2wHJZPVA2c2lVAP2WPnqFDDXJVN+WwkC2y3Y0ejOfyk1zGWVYyDwjTzsFUx qObnuHgZ6bTmghn9nSdBQkZCQUmZUxy3fp6NS//eeO3WhHjuVuYH2eZIeCV4AMJlFOFU 3SY/HgfMW1GerBKRFv4aGP7NUQSmia6/O/DD7OZ7gYIddXcq6cNx6thubPf3c1qFeFoq NnLlaYuBy63bFH34SrTLpjVKYAlxj+U4OHMeLCZgJq+FOfL0a1Mz7G88PiSAQjkDGoJF kkMw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX9T+ZFaovNZKpvrBQOeww+2I0GPiQ1iFJ7r+f/bCvCKHgqI6dS MEaMSyV8FIw6vWNqBdIeBZ4= X-Google-Smtp-Source: APXvYqzR09ce2lzpur5x2PAOEVLlS2u16B4jI7nrAp6H4fguePc3Do0IAQkkMK1pWhXZguSu72979w== X-Received: by 2002:a5e:c803:: with SMTP id y3mr14534130iol.308.1565267375836; Thu, 08 Aug 2019 05:29:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:6303:: with SMTP id p3ls3172573iog.11.gmail; Thu, 08 Aug 2019 05:29:35 -0700 (PDT) X-Received: by 2002:a5d:9690:: with SMTP id m16mr14488192ion.180.1565267375484; Thu, 08 Aug 2019 05:29:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565267375; cv=none; d=google.com; s=arc-20160816; b=oGeEiWIyhmR9C+8mVBNoZIsOr+1STjWsuJs019l6IzzaeJ/7r0o+YiaNLzZlO1qaoy HWpsC2Yb83Ab0zAiKk4WgjC6tbKYl6Wte0yXiIkXMs+wA0n1cUjj3UVqT0pysCmUTA8o GeSgKBiKWtuCQykRB00HDUgkZz1NQWhfM2/bkgrQp9is2wlC2UQO/0bVXLOAheW2NYrW 46+jCeb9vFg18hdWWjv5QMVwiAegUMal48CB8Lf7nzgT3bIcLmYyrHpEr2VziBSAfL40 MiYLNalFmqx52cMcVS9vFKwkaDgMhc5lnxft8N0Cwu1HKKAp3L+/0DtLpfbaM1QR61Os k0tw== 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=saGKUjeq7VZZzcSZN2rSTWZjwvc87tDFw0iXsfBh9P0=; b=lj3te1+Mrpze4GkLjidFqtOJxZRuItbtDhJcVJgaBNKfBtuNCw7Ev9hUX8lIYeAWTv zW4JjgH9x9twy/a/rglJdJrXOkZPhtfPZ7cjxkYkS5sGkTgf7rnh7bKEOEXpZTCrozJs OtEzbtMmGS8LhtxKf64ePuKmgWm3ApmReKFrf+QsQlkJbvjiuGkDfT7nFhneVGolAutl wbjnDiLWLG9b9WASyc1wlb4HInBEHltK9PtHuUC8vmXsxjHQCmc2r6aeqEV982vCb+R0 t0TYMlF2ziaN3IwnXc58i7mEq7dNeBMAxMUEbZr6+ZwWqQMKO3KYt0aWWu9pzM3ibA5m FQKA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VaEN5CH1; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb34.google.com (mail-yb1-xb34.google.com. [2607:f8b0:4864:20::b34]) by gmr-mx.google.com with ESMTPS id h25si3560974iol.2.2019.08.08.05.29.35 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 05:29:35 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) client-ip=2607:f8b0:4864:20::b34; Received: by mail-yb1-xb34.google.com with SMTP id s142so4003446ybc.6 for ; Thu, 08 Aug 2019 05:29:35 -0700 (PDT) X-Received: by 2002:a25:1a41:: with SMTP id a62mr9898622yba.131.1565267374911; Thu, 08 Aug 2019 05:29:34 -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: <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> From: Bas Spitters Date: Thu, 8 Aug 2019 14:29:23 +0200 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Jon Sterling Cc: "'Martin Escardo' via Homotopy Type Theory" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VaEN5CH1; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , I imagine it could be related to earlier discussions, but Valery will correct me: https://groups.google.com/forum/#!topic/homotopytypetheory/N8jw_5h2Qjs https://valis.github.io/doc.pdf On Thu, Aug 8, 2019 at 2:20 PM Jon Sterling wrote: > > Dear Valery, > > Arend looks really impressive, especially the IDE features! I look forwar= d to trying it. I like the little screen demos on the website. > > We have been curious for some time if someone could begin to explain what= type theory Arend implements --- I am not necessarily looking for somethin= g super precise, but it would be great to have a high-level gloss that woul= d help experts in the semantics of HoTT understand where Arend's type theor= y lies. For instance, I can see that Arend uses an interval, but this inter= val seems to work a bit differently from the interval in some other type th= eories. Is there any note or document that explains some of the mathematics= behind Arend? > > Nice work! And I look forward to hearing and reading more. > > Best, > Jon > > > On Tue, Aug 6, 2019, at 6:16 PM, =D0=92=D0=B0=D0=BB=D0=B5=D1=80=D0=B8=D0= =B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 wrote: > > Arend is a new theorem prover that have been developed at JetBrains > > for quite some time. We are proud to > > announce that the first version of the language was released! To learn > > more about Arend, visit our site . > > > > Arend is based on a version of homotopy type theory that includes some > > of the cubical features. In particular, it has native higher inductive > > types, including higher inductive-inductive types. It also has other > > features which are necessary for a theorem prover such as universe > > polymorphism and class system. We believe that a theorem prover should > > be convenient to use. That is why we also developed a plugin for > > IntelliJ IDEA that turns it into a > > full-fledged IDE for the Arend language. It implements many standard > > features such as syntax highlighting, completion, auto import, and auto > > formatting. It also has some language-specific features such as > > incremental typechecking and various refactoring tools. > > > > To learn more about Arend, you can check out the documentation > > . You can also learn a lot > > from studying the standard library > > . It implements some basic > > algebra, including localization of rings, and homotopy theory, > > including joins, modalities, and localization of types. > > > > Frequently asked questions (that nobody asked): > > * Why do we need another theorem prover? We believe that a theorem > > prover should be convenient to use. This means that it should have an > > IDE comparable to that of mainstream programming languages. That is why > > we implemented IntelliJ Arend > > . This also means > > that the underlying theory should be powerful and expressive. That is > > why Arend is based on homotopy type theory and has features such as an > > impredicative type of propositions and a powerful class system. > > * Does Arend have tactics? Not yet, but we are working on it. > > * Does Arend have the canonicity property, i.e. does it evaluate > > closed expressions to their canonical forms? No, but it computes more > > terms than ordinary homotopy type theory, which makes it more > > convenient in many aspects. > > If you want to know about language updates, you can follow us on > > twitter . Questions, suggestions, and > > comments are welcome at google groups > > . > > > > -- > > 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/9d23061c-4b7a-4d69= -9c22-f28261ad3b33%40googlegroups.com . > > -- > 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/msgi= d/HomotopyTypeTheory/06e24c98-7409-4e75-88ee-a6e1bb891e1e%40www.fastmail.co= m. --=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/CAOoPQuSLoX8gKy54NQM6SNoi43wVA0A1Ad59qKs6prULkh6zBw%40ma= il.gmail.com.