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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yw1-xc3a.google.com (mail-yw1-xc3a.google.com [IPv6:2607:f8b0:4864:20::c3a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7e910959 for ; Thu, 8 Aug 2019 15:23:30 +0000 (UTC) Received: by mail-yw1-xc3a.google.com with SMTP id b195sf68699353ywa.16 for ; Thu, 08 Aug 2019 08:23:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565277810; cv=pass; d=google.com; s=arc-20160816; b=G4uFoh8ZkRD5qS+BN/BBpVRHpbX69BavdtPF0NWT8giAMOAqSUUatBYoFPmqjyPkkx tMtda3qCray+N1uoOkDkFTAoeMUs3mcysUFWzTUyJovw5gg/6Buys4aheaoiRIFWRLJp ejKtoT+0U09t0+yr8F4UoLeMpaWRacj5UAY+GNjO17lXKdPGF8JtbQlecs6bfWZH2h0+ noQFn/nHAleWYAqBZxR6iqG3mAk7sonZewsq5DeMK+DrqCj75PXP+cySn9YmC+pVZg4i p428aFmIa8gSgZ0hzFSmgzPrHDx0eWLENuc7eOyVc1+jgZvXWMWFfdLg8kG1JIyDS5gD e0TA== 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 :dkim-signature; bh=mejPPr5E9ua+dpb22+10t/yqBhDT/Kudg4MXzVbMr6s=; b=pWkByk2QD/5LhLtXIA2/4qRxPR97qrpu1Qo+fsqF8VzvosZEONpMKpiuC/8JCuAA7V jTv6awx/6cNoX7rBkAcldslP5ChcqNHBklb/ue9dLeNDVAXvUSYX8R2H8KaWRM6+2iBX zrooavuz9KO71HQaXJSs9449hFlcUTT8+gEy51mioiJjYniBLJrTE5Drz/XxXGuhGuFR FKexnNUTIwoosyV+1qdte8lMGExikYL2mgWdBSY02jzawmwcaFGBPea/QKd8KG7EIHNV 4h6QDq2qSGHR81FIQ0tKIdJebUIiGnr5cD6zankn7wWRuMvrh9bO4HYsmnqNU5RaYhwE 5iPA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=MgTJjPF1; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) smtp.mailfrom=valery.isaev@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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=mejPPr5E9ua+dpb22+10t/yqBhDT/Kudg4MXzVbMr6s=; b=oEbe7f1duYgX1Cq6v1BqWenzasvju4vI8EghPFvKnCGyzEGNVw6GK1pJFb8uomYETq s9Zel8xAhY3hMv/Yr44bmm7De9GDH3d5LX66FjcdZ513GtaQR+H258kk2yMiCmaBfMse Q8r7LcZZT2NuU9cNeVfFYQiIvQQ7tCINJEo/3cbH2LsONMefxojeMdAN+2sAv42a53im SEsbJ6mIoOFPaU9ixJYEEfYYqDqYN79Mv/vBP4Kg8kpwwXNXj1bSnJwPxhM0PkXn/L1z qUl0at7hp2bJ7NH96ayriI/5sxA+2UbPf/3Xx74Mwwtm+B/+qEHwiLZpVtN/Fpkv+mHA gP3Q== 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:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=mejPPr5E9ua+dpb22+10t/yqBhDT/Kudg4MXzVbMr6s=; b=hgqMgSeVcOpi5+c6bPPPgSa2LFcTsaDIu6Z0BherK3jZivPghJ2oC4pwFKhhAcpx4h Sj8v/eMH/a0ejVkKpcrtnu2fmTSN/fnUoTCPUZAb+tpXZ4BTZ05qpYgWVYM3pxggfZqv sj/7U9nfCaZqVXa0N8FhVq+2q3noulXZU1/2yEGGNkcH53Kmk5yOlkta5ki3R5zmqrTs Rem/eX7QpIdDiSq37o1jsSjjXZfwVwFQ3EBmklGg03sP+6Cbr9+MqmScAJsfv6mkSjKi 7QlYPKHi9EBCCkQnIYfqRHMJzA6VuQKmUU2hTZFI/h728XA1IF0ASmlYVhllPGNwJCl+ JqrA== 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=mejPPr5E9ua+dpb22+10t/yqBhDT/Kudg4MXzVbMr6s=; b=mEbrfmiBvAVRiXFfGWXDRvZW1paP5u5DLfU4eSo/5oeOoSy3gb+EBXQTP0iHnivQBf WJsGxuf2RjWZYTxv7u8azsEwauo77K29afaYDxIYj7rJ+KAp9rlt36E2iE/fBY47rbBj No6buKAdLWJK6q7EtykYxVrsf7u3L5jA4TfwvdgKeia+HUl0PCx+0I1zsqQIXxNhotiN NZJMJvWJoXYhwuKR7kkmMH+KPBuforaNfQyLyialyie/gFm08ikHZFF0/+4RpsyRvJg9 9IRKdEu0/OL/Z0As/T8W9AMDT3Qy+au4uVYjzIOcVLEqaolaBlkBaCLFSdZdhm1WFFqZ YXRg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXFaHLNvQIkPjySSrMsswRiXnVC6PyBUCAsNipXzaX/ZYxdie7U /aP8/r/MHVYUIL3PTK0gphY= X-Google-Smtp-Source: APXvYqyrmigg7vE7pb6EPZ2gdoCdsiKU2CHWDlYp3oTCq7/8gyNMl5f1xvg+WHCI4/Cbe6cVd8iJHA== X-Received: by 2002:a25:81c2:: with SMTP id n2mr10606686ybm.378.1565277809841; Thu, 08 Aug 2019 08:23:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:42c7:: with SMTP id p190ls63043yba.7.gmail; Thu, 08 Aug 2019 08:23:29 -0700 (PDT) X-Received: by 2002:a25:bacc:: with SMTP id a12mr2553913ybk.501.1565277809467; Thu, 08 Aug 2019 08:23:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565277809; cv=none; d=google.com; s=arc-20160816; b=AaIjmIVsWLxpW949OG+5c1WhzEL+CC3pePqX4Gg4LLen84fg9tMk0tbrXa9LZxcc+S yshVqFI9RdlQJvRl8SCG3+juG15Z3OaGkVf4Ae1XOzdUf4vUqz7KmhoRGSnVLXExn9J2 J3ZhUPoRlu+LZbnhtfjwEyNGWNd4Oa+Nj5JXOTr7v4mzXpnb1uP4ZLYAWhnTTYSn53D/ a9rs0uFTaLM9dar92EbSVmaBQBuonCr2EokmT74yHTKL+ntaREt3B2jD1B7vch/u95n3 rgDz79S/gbJKlHXS4rEM9SNimbKVU2KWXUSTKNlgGhPqdlw7ZW8tgBQAIM5RscqLx3k/ gwEA== 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=5p02km90N0wJ0Gm4HcFo01hBfkWqxzKGF+RX0CJRzLQ=; b=hBCBs6FxM/TqNdM75MUvJ7qrAjEtwrVJcSbcHu8DveLaj58NyPsIz6TWxaCf8LF657 9/vLGxlegyKgc9AXftlf9ICCJtJSmeKXWGpyiuVayEw105C+1v9MWUXdwClfFq7xXhdb v3sK3Jt/1t6aXnVgrWN08ETrP1unimhNTzW29qJCz4DgNpKjBSwQsFTsHuVgjTzII01t KklTJxSadaPWURxJD7AJvDaabCOIh+kZlpoRJw2+vcbd3awMbNOqMdolKQ8ZtO+QtaWM E5UQJnrSx11s40cFgQVHRfonHbETSBPmL04Z0NnEDSyoX9YioraYANJ+Mx3wFODWrvGA rNpg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=MgTJjPF1; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x32d.google.com (mail-ot1-x32d.google.com. [2607:f8b0:4864:20::32d]) by gmr-mx.google.com with ESMTPS id r1si5352691ywg.4.2019.08.08.08.23.29 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 08:23:29 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) client-ip=2607:f8b0:4864:20::32d; Received: by mail-ot1-x32d.google.com with SMTP id x21so26779765otq.12 for ; Thu, 08 Aug 2019 08:23:29 -0700 (PDT) X-Received: by 2002:a5e:a70b:: with SMTP id b11mr11679924iod.286.1565277809048; Thu, 08 Aug 2019 08:23:29 -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: Valery Isaev Date: Thu, 8 Aug 2019 18:22:52 +0300 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Jon Sterling Cc: "'Martin Escardo' via Homotopy Type Theory" Content-Type: multipart/alternative; boundary="000000000000c88122058f9ca3ee" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=MgTJjPF1; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) smtp.mailfrom=valery.isaev@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: , --000000000000c88122058f9ca3ee Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable =D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 18:11, Jon Sterling= : > Hi Valery (and Bas), > > Thanks very much for the reference! Can you say a bit more about the > interpretation in model categories? I have the following specific questio= ns: > > - By "Cartesian model category" do you refer to the pushout-product axiom= ? > I apologize for my ignorance, model categories are not my area of experti= se. > > Yes. > - In most models of HoTT that I'm familiar with, including simplicial set= s > and several versions of cubical sets, the interval is not fibrant. What > interpretation do have in mind for I? (btw, sorry if this has been > discussed before!). > You can take any contractible fibrant object such that the map 1+1 -> I is a cofibration. Such an object always exists (just factor the map 1+1 -> 1 as a cofibration followed by trivial fibration), so the only additional assumption is that the exponential (-)^I exists and the pushout-product axiom holds. > > Thanks, > Jon > > > On Thu, Aug 8, 2019, at 10:45 AM, Valery Isaev wrote: > > Yes, Arend implements the theory described in this document. > > Semantically, the additional constructions of this theory correspond to > > the assumption that the model has a fibrant object I such that maps > > : X -> X \times I have the left lifting property with respect > > to fibrations, and the path object functor is given by (-)^I. So, the > > usual interpretation in model categories (and other similar models) of > > HoTT extends to an interpretation of this theory if the model category > > is a Cartesian model category. > > > > Regards, > > Valery Isaev > > > > > > =D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 15:29, Bas Spit= ters : > > > I imagine it could be related to earlier discussions, but Valery will > > > correct me: > > > https://groups.google.com/forum/#!topic/homotopytypetheory/N8jw_5h2Qj= s > > > 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 > 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 type theory Arend implements --- I am not necessarily lookin= g > 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 interval seems to work a bit differently from the > interval in some other type theories. 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 t= o > > > > > 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 include= s > 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 univer= se > > > > > 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 theor= em > > > > > 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 Goog= le > > > > > 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-9= c22-f28261ad3b33%40googlegroups.com > < > https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9= c22-f28261ad3b33%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter > >. > > > > > > > > -- > > > > 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 HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > > > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/06e24c98-7409-4e75-8= 8ee-a6e1bb891e1e%40www.fastmail.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 HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSLoX8gKy54NQM= 6SNoi43wVA0A1Ad59qKs6prULkh6zBw%40mail.gmail.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/msgid/HomotopyTypeTheory/CAA520ft6xBR1fJz4N0c= 5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.com > < > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520ft6xBR1fJz4N0c= 5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.com?utm_medium=3Demail&u= tm_source=3Dfooter > >. > > -- > 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/d0fd1d18-136b-41fa-b= 721-f64b9c487376%40www.fastmail.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/CAA520fuU-BEcdg6mrAkTxmqpDhG9pHpD-1a%3DX7ZU-n8q57dKsg%40= mail.gmail.com. --000000000000c88122058f9ca3ee Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


=
=D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2= 019 =D0=B3. =D0=B2 18:11, Jon Sterling <jon@jonmsterling.com>:
Hi Valery (and Bas),

Thanks very much for the reference! Can you say a bit more about the interp= retation in model categories? I have the following specific questions:

- By "Cartesian model category" do you refer to the pushout-produ= ct axiom? I apologize for my ignorance, model categories are not my area of= expertise.


Yes.
=C2=A0
- In most models of HoTT that I'm familiar with, including simplicial s= ets and several versions of cubical sets, the interval is not fibrant. What= interpretation do have in mind for I? (btw, sorry if this has been discuss= ed before!).

You can take any contracti= ble fibrant object such that the map 1+1 -> I is a cofibration. Such an = object always exists (just factor the map 1+1 -> 1 as a cofibration foll= owed by trivial fibration), so the only additional assumption is that the e= xponential (-)^I exists and the pushout-product axiom holds.
=C2= =A0

Thanks,
Jon


On Thu, Aug 8, 2019, at 10:45 AM, Valery Isaev wrote:
> Yes, Arend implements the theory described in this document.
> Semantically, the additional constructions of this theory correspond t= o
> the assumption that the model has a fibrant object I such that maps > <id,left> : X -> X \times I have the left lifting property wi= th respect
> to fibrations, and the path object functor is given by (-)^I. So, the =
> usual interpretation in model categories (and other similar models) of=
> HoTT extends to an interpretation of this theory if the model category=
> is a Cartesian model category.
>
> Regards,
> Valery Isaev
>
>
> =D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 15:29, Bas Spi= tters <b.a= .w.spitters@gmail.com>:
> > I imagine it could be related to earlier discussions, but Valery = will
> >=C2=A0 correct me:
> > https://groups.googl= e.com/forum/#!topic/homotopytypetheory/N8jw_5h2Qjs
> > https://valis.github.io/doc.pdf
> >
> >=C2=A0 On Thu, Aug 8, 2019 at 2:20 PM Jon Sterling <jon@jonmsterling.com>= wrote:
> >=C2=A0 >
> >=C2=A0 > Dear Valery,
> >=C2=A0 >
> >=C2=A0 > Arend looks really impressive, especially the IDE feat= ures! I look forward to trying it. I like the little screen demos on the we= bsite.
> >=C2=A0 >
> >=C2=A0 > We have been curious for some time if someone could be= gin to explain what type theory Arend implements --- I am not necessarily l= ooking for something super precise, but it would be great to have a high-le= vel 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 i= nterval, but this interval seems to work a bit differently from the interva= l in some other type theories. Is there any note or document that explains = some of the mathematics behind Arend?
> >=C2=A0 >
> >=C2=A0 > Nice work! And I look forward to hearing and reading m= ore.
> >=C2=A0 >
> >=C2=A0 > Best,
> >=C2=A0 > Jon
> >=C2=A0 >
> >=C2=A0 >
> >=C2=A0 > 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:
> >=C2=A0 > > Arend is a new theorem prover that have been deve= loped at JetBrains
> >=C2=A0 > > <https://www.jetbrains.com/> for quite= some time. We are proud to
> >=C2=A0 > > announce that the first version of the language w= as released! To learn
> >=C2=A0 > > more about Arend, visit our site <https://= arend-lang.github.io/>.
> >=C2=A0 > >
> >=C2=A0 > > Arend is based on a version of homotopy type theo= ry that includes some
> >=C2=A0 > > of the cubical features. In particular, it has na= tive higher inductive
> >=C2=A0 > > types, including higher inductive-inductive types= . It also has other
> >=C2=A0 > > features which are necessary for a theorem prover= such as universe
> >=C2=A0 > > polymorphism and class system. We believe that a = theorem prover should
> >=C2=A0 > > be convenient to use. That is why we also develop= ed a plugin for
> >=C2=A0 > > IntelliJ IDEA <https://www.jetbrains.com= /idea/> that turns it into a
> >=C2=A0 > > full-fledged IDE for the Arend language. It imple= ments many standard
> >=C2=A0 > > features such as syntax highlighting, completion,= auto import, and auto
> >=C2=A0 > > formatting. It also has some language-specific fe= atures such as
> >=C2=A0 > > incremental typechecking and various refactoring = tools.
> >=C2=A0 > >
> >=C2=A0 > > To learn more about Arend, you can check out the = documentation
> >=C2=A0 > > <https://arend-lang.github.io= /documentation>. You can also learn a lot
> >=C2=A0 > > from studying the standard library
> >=C2=A0 > > <https://github.com/JetBrains/are= nd-lib>. It implements some basic
> >=C2=A0 > > algebra, including localization of rings, and hom= otopy theory,
> >=C2=A0 > > including joins, modalities, and localization of = types.
> >=C2=A0 > >
> >=C2=A0 > > Frequently asked questions (that nobody asked): > >=C2=A0 > > * Why do we need another theorem prover? We belie= ve that a theorem
> >=C2=A0 > > prover should be convenient to use. This means th= at it should have an
> >=C2=A0 > > IDE comparable to that of mainstream programming = languages. That is why
> >=C2=A0 > > we implemented IntelliJ Arend
> >=C2=A0 > > <https://arend-lang= .github.io/about/intellij-features>. This also means
> >=C2=A0 > > that the underlying theory should be powerful and= expressive. That is
> >=C2=A0 > > why Arend is based on homotopy type theory and ha= s features such as an
> >=C2=A0 > > impredicative type of propositions and a powerful= class system.
> >=C2=A0 > > * Does Arend have tactics? Not yet, but we are wo= rking on it.
> >=C2=A0 > > * Does Arend have the canonicity property, i.e. d= oes it evaluate
> >=C2=A0 > > closed expressions to their canonical forms? No, = but it computes more
> >=C2=A0 > > terms than ordinary homotopy type theory, which m= akes it more
> >=C2=A0 > > convenient in many aspects.
> >=C2=A0 > > If you want to know about language updates, you c= an follow us on
> >=C2=A0 > > twitter <https://twitter.com/ArendLang= >. Questions, suggestions, and
> >=C2=A0 > > comments are welcome at google groups
> >=C2=A0 > > <https://groups.googl= e.com/forum/#!forum/arend-lang>.
> >=C2=A0 > >
> >=C2=A0 > > --
> >=C2=A0 > > You received this message because you are subscri= bed to the Google
> >=C2=A0 > > Groups "Homotopy Type Theory" group. > >=C2=A0 > > To unsubscribe from this group and stop receiving= emails from it, send
> >=C2=A0 > > an email to HomotopyTypeTheory+unsubs= cribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bun= subscribe@googlegroups.com>.
> >=C2=A0 > > To view this discussion on the web visit
> >=C2=A0 > > https://groups.google.com/d/msgid/Homotop= yTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com <= ;https://groups.google.c= om/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40google= groups.com?utm_medium=3Demail&utm_source=3Dfooter>.
> >=C2=A0 >
> >=C2=A0 > --
> >=C2=A0 > You received this message because you are subscribed t= o the Google Groups "Homotopy Type Theory" group.
> >=C2=A0 > To unsubscribe from this group and stop receiving emai= ls from it, send an email to HomotopyTypeTheory+unsubscribe@goo= glegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe= @googlegroups.com>.
> >=C2=A0 > To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/06e24c98-7409-4e75-88ee-a6e= 1bb891e1e%40www.fastmail.com.
> >
> >=C2=A0 --
> >=C2=A0 You received this message because you are subscribed to the= Google Groups "Homotopy Type Theory" group.
> >=C2=A0 To unsubscribe from this group and stop receiving emails fr= om it, send an email to HomotopyTypeTheory+unsubscribe@googlegr= oups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@goog= legroups.com>.
> >=C2=A0 To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSLoX8gKy54NQ= M6SNoi43wVA0A1Ad59qKs6prULkh6zBw%40mail.gmail.com.
>
>=C2=A0 --
>=C2=A0 You received this message because you are subscribed to the Goog= le
> Groups "Homotopy Type Theory" group.
>=C2=A0 To unsubscribe from this group and stop receiving emails from it= , send
> an email to HomotopyTypeTheory+unsubscribe@googlegroups.co= m.
>=C2=A0 To view this discussion on the web visit
> https://groups.google.com/d/msgid/Homotop= yTypeTheory/CAA520ft6xBR1fJz4N0c5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mai= l.gmail.com <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520f= t6xBR1fJz4N0c5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.com?utm_med= ium=3Demail&utm_source=3Dfooter>.

--
You received this message because you are subscribed to the Google Groups &= quot;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/d0fd1d18-136b-41fa-b721-f64b9c487376%40www.fastm= ail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAA520fuU-BEcdg6mrAkTxmqpDhG9pH= pD-1a%3DX7ZU-n8q57dKsg%40mail.gmail.com.
--000000000000c88122058f9ca3ee--