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-lj1-x237.google.com (mail-lj1-x237.google.com [IPv6:2a00:1450:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id dcc4fbde for ; Thu, 8 Aug 2019 12:20:29 +0000 (UTC) Received: by mail-lj1-x237.google.com with SMTP id l10sf18652216ljj.10 for ; Thu, 08 Aug 2019 05:20:29 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565266828; cv=pass; d=google.com; s=arc-20160816; b=uYNbcLvVu/nuYnOd7fCvWLFX/n2bVtminN+uu7BjdpgeWyogr34eQb1Uw3CBGkhsi2 h1a4FBcIQE3TWBsBtX3rnvjVk/WNygheR8us/kUeCPFNla65bvyrWuxcZC5x87AjxVF8 W+CrsWimuV1wz2E4svFDa17g4L9WcCFgNhNjs85pJ3P6EgqAVvLxxL3ejBArBYoVISzQ oQmDbKqWTt9OtxA6c1qwqzdRd1o/drsLnF3f7KGBnwxGcv1mmYtFIVRCqblrVxdNYtzM xeh3qDx0bCWahqwjKGM6zyZaZTzy+uTq/koJXO8c+o14oQds1SveOFIZI8VuXqTjAGhL 0H6A== 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:subject:to:from :date:references:in-reply-to:message-id:mime-version:user-agent :sender:dkim-signature; bh=fWFIiGToeBc5nuyTTSSVt2Lfes60DmwdqJvK6RMLpK0=; b=l1GEw4KGfCgzpmEAB49Un6xUlxxBvP5zeKSTf2jeWaDj5TeVoTizl7wb/YvNasGgNw rsKf9lGl0KpufkNpOY//3fF0vS/JCXblsTs/e6rmc0ttLcugpp4OphwFz91ufhOS5cxG SD5n2WSHtRqUxcFT7ceOZdBLlUDcBvtwfLJWDiP4BoyTKgCOW9Um9Grr5EMaAlduDiE8 pNipUZ17bodnHswxGceikzdV+j/iSj8K2KxI1vrzEqO04p+oAwsyyJS41UnY2u0uz9F0 dh+vul3knWf9TVH4ObLifcHZwvQhUnphqfi8N5lP8547DffJWIHeLAi+TRiypohgYvu2 mxbw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=Zx+Xv8GH; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:user-agent:mime-version:message-id:in-reply-to:references :date:from:to:subject:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=fWFIiGToeBc5nuyTTSSVt2Lfes60DmwdqJvK6RMLpK0=; b=XBhbLrwcgY5OqEgLcor5POrQPqH7omj9YJWEQq80O1Qi/igQMY3vcGTFdsmPTwMR/C w56VukV8yeVA7w2y39o0/UGIGdfuMM8gN4vnXj1Ehl3EK88TNqFsgYbObUvvcedh2ku0 NI7/JZjR/OXZZxdKdPqkwabIxhB8DS8pWbTA+yBaw3/ch0AcXol+Q/IWEzTFMH5u69QJ ssEXCbqNO7UM6ElrnrcBWMzOAgEjieJoG0Yfc6ZaRvhpSJJdIhc5aJuqKH0AVZAr+wHT X9nj7cX+2tpOydZMZUocrZy306/8LeSkpwMfGkzE7mSvjhnpns9OMYJenYuppFOn581J tR4A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:user-agent:mime-version:message-id :in-reply-to:references:date:from:to:subject :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=fWFIiGToeBc5nuyTTSSVt2Lfes60DmwdqJvK6RMLpK0=; b=uiwpDRLzM/gbgvm4xOaAJ+DSjaXa2y3MIyV01Cm6U5uqyf1hQkqaHtCL6YzcTbLNXE 6FstsSeJJS+ViO2i3SwgjU9lS8z63ozUDkbsDJnsDUXMwvsday216YhNcPeiI1Q9yoYe Dfse1duVqVGNsotPGEe9HlxkJOrswHC3SOsrZOw1zAGKCYQ+qr2pn6QRFcYklPDgrzal AfTLvwALfu6gpiZPhLrxqXxvC4kOFgkCurOFbcJ4d3KLsTG90iYuT2BAbxO0HWVt+qdC naraEO7HAFqIAelpDXAhZ18Dycvfcghk7I1drloyEOOwjmnYU6iGCQJxDgn6cAQ2Q3sK 2UXQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW/D67i1caHZ3youXI5GUpGdoGE53+GARhr4Alv/e4QxWQ7rxbc WmYuooOjfzMoZbbV276AToE= X-Google-Smtp-Source: APXvYqyawzjsnZxZJ2KltpVT8KdKFLDYeTZZBj1ZTEl3AwXGQc5Nsa6CR7Q+xDboSYIUk0L5t/hunA== X-Received: by 2002:a2e:8986:: with SMTP id c6mr299097lji.59.1565266828631; Thu, 08 Aug 2019 05:20:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:96d5:: with SMTP id d21ls10656223ljj.16.gmail; Thu, 08 Aug 2019 05:20:27 -0700 (PDT) X-Received: by 2002:a2e:86cc:: with SMTP id n12mr7973779ljj.146.1565266827649; Thu, 08 Aug 2019 05:20:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565266827; cv=none; d=google.com; s=arc-20160816; b=PS1pdJDJthqWo0G1RS+Bj7WLpw95E8ees0JhtVxFzNV1/+iJJUll0q6XNMvJ84MikH s97KWdFiQqodDUGzIkg1KlNCN6H/qCvcpm71TdF4oaaoJG0YvTAW9UEhBGW4dU3Ox19l kzExr79n+8KhG1wMvSI9oh/pDJeA+7rPx6+yG7pMth4UeyHuLexgPbjKcHyu56g5bP+h pfXNDJMysu+zDFoLALJLU2lKDhdlDad6PX/NHBck9ecacTw+ehNdguLjnDioUuBSNLwc z8MqCdos31rqZFKqJrK4ZvL7ChEmTUg8sFDjLyY6nGHfOWciNY5BcRUCfUqf6wolOeL/ SBqQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:to:from:date:references :in-reply-to:message-id:mime-version:user-agent:dkim-signature; bh=iYE6HmDEm/zT/CpXx6qF9yfn6cQwSneSwujvLDT4y+Q=; b=ECZKkoMHkqBU3yBzpwOpfDm+QNPTBVx9dElefhoJwJgYp/lqHimNzBRJq5MzfyhTNq tNM8FRmlhMWhiPckaaEL3zu9fLBpNrbhjH+Fcsvwu133YW2Ee8r8DJy2khTTmkB9x9vW hUCQrZfuGt4hbknAzjwjofSB9fn9tnf+KS2jwH5/IKE/HiiJL7BgOW7hwQkdJBXt5u2W +i74MEB2/V7QmCJ4mO0VgUeb/v4KgLGJ+RRccXp53/++ueIdpJNgckqOYU5vUXiqo1P/ u4zzbrcb3hgsLLvMrERhmuPIT1JtyGKtpifLvipTaGQld7ua9Ln5DUMCr1s7je7Hp2M6 DWng== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=Zx+Xv8GH; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from wout2-smtp.messagingengine.com (wout2-smtp.messagingengine.com. [64.147.123.25]) by gmr-mx.google.com with ESMTPS id q7si1846267lji.5.2019.08.08.05.20.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 05:20:27 -0700 (PDT) Received-SPF: neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=64.147.123.25; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.west.internal (Postfix) with ESMTP id A03FE481 for ; Thu, 8 Aug 2019 08:20:24 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute2.internal (MEProxy); Thu, 08 Aug 2019 08:20:24 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduvddrudduhedghedvucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne goufhushhpvggtthffohhmrghinhculdegledmnecujfgurhepofgfggfkjghffffhvffu tgfgsehtqhertderreejnecuhfhrohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjoh hnsehjohhnmhhsthgvrhhlihhnghdrtghomheqnecuffhomhgrihhnpehjvghtsghrrghi nhhsrdgtohhmpdhtfihithhtvghrrdgtohhmpdhgohhoghhlvgdrtghomhdpghhithhhuh gsrdhiohdpghhithhhuhgsrdgtohhmnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjohhn sehjohhnmhhsthgvrhhlihhnghdrtghomhenucevlhhushhtvghrufhiiigvpedt X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id E30A45C0099; Thu, 8 Aug 2019 08:20:23 -0400 (EDT) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.6-808-g930a1a1-fmstable-20190805v2 Mime-Version: 1.0 Message-Id: <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> In-Reply-To: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> Date: Thu, 08 Aug 2019 08:20:23 -0400 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] New theorem prover Arend is released Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=Zx+Xv8GH; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.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: , Dear Valery, Arend looks really impressive, especially the IDE features! I look forward = 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 t= ype theory Arend implements --- I am not necessarily looking for something = super precise, but it would be great to have a high-level gloss that would = help experts in the semantics of HoTT understand where Arend's type theory = lies. For instance, I can see that Arend uses an interval, but this interva= l seems to work a bit differently from the interval in some other type theo= ries. Is there any note or document that explains some of the mathematics b= ehind 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=20 > for quite some time. We are proud to=20 > announce that the first version of the language was released! To learn=20 > more about Arend, visit our site . >=20 > Arend is based on a version of homotopy type theory that includes some=20 > of the cubical features. In particular, it has native higher inductive=20 > types, including higher inductive-inductive types. It also has other=20 > features which are necessary for a theorem prover such as universe=20 > polymorphism and class system. We believe that a theorem prover should=20 > be convenient to use. That is why we also developed a plugin for=20 > IntelliJ IDEA that turns it into a=20 > full-fledged IDE for the Arend language. It implements many standard=20 > features such as syntax highlighting, completion, auto import, and auto= =20 > formatting. It also has some language-specific features such as=20 > incremental typechecking and various refactoring tools. >=20 > To learn more about Arend, you can check out the documentation=20 > . You can also learn a lot=20 > from studying the standard library=20 > . It implements some basic=20 > algebra, including localization of rings, and homotopy theory,=20 > including joins, modalities, and localization of types. >=20 > Frequently asked questions (that nobody asked): > * Why do we need another theorem prover? We believe that a theorem=20 > prover should be convenient to use. This means that it should have an=20 > IDE comparable to that of mainstream programming languages. That is why= =20 > we implemented IntelliJ Arend=20 > . This also means= =20 > that the underlying theory should be powerful and expressive. That is=20 > why Arend is based on homotopy type theory and has features such as an=20 > 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=20 > closed expressions to their canonical forms? No, but it computes more=20 > terms than ordinary homotopy type theory, which makes it more=20 > convenient in many aspects. > If you want to know about language updates, you can follow us on=20 > twitter . Questions, suggestions, and=20 > comments are welcome at google groups=20 > . >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9= c22-f28261ad3b33%40googlegroups.com . --=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/06e24c98-7409-4e75-88ee-a6e1bb891e1e%40www.fastmail.com.