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-lf1-x137.google.com (mail-lf1-x137.google.com [IPv6:2a00:1450:4864:20::137]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d604dadd for ; Wed, 7 Aug 2019 22:13:55 +0000 (UTC) Received: by mail-lf1-x137.google.com with SMTP id g13sf10123962lfb.2 for ; Wed, 07 Aug 2019 15:13:55 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565216034; cv=pass; d=google.com; s=arc-20160816; b=NIO7svetOD0J1zWE9T904dqKqjV9CnZBxyMVcCt+0/UTjUYjevSxJWkjOGycymYBcK Hc++1RPhpSqLpQ7so600PaMX6mgIGXXJuWm+NoMnW85+9wXQFUgHGb0Ejhxc2NXK0njJ Wuue/hoR4itV556a+GomLHkkOqTC/XbC8xMUCgIk061j0rs7jqz/pBUk5J5jLP0Ulfez lWHD0q/rhukV78oZDWya/DGDPZrJ8qrZXq8OzXUxMWcTztq3s8Kh/tH9unPMDm5DUPRB 8NFyk8P3QTnN1POpaLXr4GZsrjny4M4ukPzdkIaD+NBqnJInmPnKQArqmMsoSP3Fc5eY lIdA== 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=iO8CWFi0WKNQogq62eOM3HRKvIzIyrwwdOhLKWovDYw=; b=O/bbYXOA8k+vYDqK3CGRDwNGeURphgcXASVKnKSU2pItRDg8/dpw3aWmz2Lr3bhrA3 kib3bV5hKhOCvWeSi5e5QO9gwmRac5ido4ksIBRK2VqcfEETrcXJR4qcEjyhdJwsxrRw a7BxdfietTEP1Y+pxaCZl16TUUAkoJv02Se+3+ais3MWBLcgjXs1n3seRbySs0uVbm1R AlRMAtKm8YzuoCD1ozQEvH7WNB8gIkwaqsXFx6FFI+Kilvt/AuaUo4k+emDePssqu1Ru AQ5JFWb370Fa4tvKn38qxrwomrqAGZveBjXREh0x6aLEVdeKM6FtZodRfkFlOP2SHsHU AlcQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=N+pwW9OX; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) smtp.mailfrom=nicolai.kraus@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=iO8CWFi0WKNQogq62eOM3HRKvIzIyrwwdOhLKWovDYw=; b=HvULgm+PDRPEOIObQ8iZOi8gKX6mQCO+W+zv/WR2D1htinAWaWoSgMsV4hwxatxXMw t7fCb7VPOKZGq36uoofsNKOXOauMNeBFHVwTY/lXxvnohEB3T4OCHXOW/qlb+PabkAG7 BvuotjzyRzZMflapmcMmFaaWfyFRWa54Vfgm/kvoobij57cWi56c39q0IL+wBeMq/riB 0oniifKxowJEV1tYZOI6cgDbzc93lIrXp8RmJCoWUW6Hg0VVreQKu5ptRysmFajug7nZ 3N0oh2QV3+twiaUVK+DxJlrKrALv3sOC9LkCnYznsd8KUYKWWhlAyxwaxDarRJZLQEVu ni4g== 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=iO8CWFi0WKNQogq62eOM3HRKvIzIyrwwdOhLKWovDYw=; b=FEOxSF512rQ4uLxocLGi1yyby4r9j64f+ow3/Xy5VOr6heP2HxBdgNTqKXuZAwbyPG R4WVgqutC8zR5etauc1g/JixmPYyebxuAmA50q0QbAnn5wM4BrLMt0qRJbT0EhMe/GUb YQh6VZ+TU99rRcdxa10H0T1vqbaDaw4gREokaH1ycuyATz7Oga52I8rHAcJeIfYt2r+/ yPKS89HQ/xVkWlz0qyEmhDvCyA12XcoYac1UtV4U3MdOba/T1UooGL6e/qMjX5RWyEu2 Z0bh/J3KtaLc7KRZFjRzaiJ05+n0nnTEMBgnoIgY5Xz0Rwh7EC6CYkI46VENDMj35omn ffAA== 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=iO8CWFi0WKNQogq62eOM3HRKvIzIyrwwdOhLKWovDYw=; b=eir+4DBd8FIzoA+gm5I3C41CEPfgyhls0RxQYiejYkzJC55gAJFk+xFSUXH1bJAhq7 9yXxGAjg/pRXW6dXI5EL8Js8HrjDONgjfWxZAKn2/uW2KHdGGduCLFcMtLAgJUNYIxhr XMZKn3rsksmXDBg1yV3xbDlDBnZgtJs0qE5Vx7m+X+y9thH3pBLtXetAA7br7/xIt58q nPzRPWkTVH/Mjowp91TrevryTfeP+SNNZRvx5umYyvcsvZx9LGclw/quwAV9FcwYoJAY gPSgrX9NLZ3K/ychEepwMBiNuxoOPOKIEc5dlgSlDzx3FZdpeSPEd8GcuPs3Vir/yn0K /jdA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXLZSagA5FuNBfjvuRA+SbvfJWdWdr7v9vxWxDgbseU9tfZywu+ Q6+bmOCqb5ly4sYAiZav+EU= X-Google-Smtp-Source: APXvYqzmq2pu/e/1rWOmhtm+L3ad0+0tfWrX4kVyTpU4hZZFbQqLu0wtDBd8fhl0LfZMQmlwDAlm8Q== X-Received: by 2002:a05:6512:48f:: with SMTP id v15mr7299071lfq.37.1565216034627; Wed, 07 Aug 2019 15:13:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:65da:: with SMTP id e87ls10434565ljf.1.gmail; Wed, 07 Aug 2019 15:13:54 -0700 (PDT) X-Received: by 2002:a2e:864d:: with SMTP id i13mr5983741ljj.92.1565216033870; Wed, 07 Aug 2019 15:13:53 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565216033; cv=none; d=google.com; s=arc-20160816; b=xnEMXxIr4log/NthdNgKJft0pmE8kh7PSW5Y5usgL0ByWTiRbsl+DyYRQH8xN+Rha5 hQ6cHc8QsRMAUSBQu9bEpM0F9jOl7TqbkoZbdf4zn2i1YhOWZkUkkyMrJQJfEFx4GZUV VKpG2KR6CWji1NU3fspo7Y/hXG5Db9BMesuVJKtI4b+CW2IS5+FlUZmQfADbcKVijRPZ 3c7qowEyWhFU44z4FVfGnEIBuwA4X0hVLnMw9Ei+uOwt1eeMKYaKA6oajlk2zrQapsny S9NkfBt3dwu8c8e9E/pqVSiaeAKMbUf3AdIp5sWwRF9pTYRGsYzJleQzqTGE5U8xXl1o BQtg== 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=rLnPSkPVUF95UcOdkgpJk0w6ggCrb7iRaMe4t7xYOhw=; b=OOdUsWQrHisFduMwNnBQ1unzSNnk4eizhOGRf7Y0ChQYtP6m/9MsE713vntCjEWOvo whnBpi1qwEG39P/NXk3Ekd70nRnrFwgmsUH3WHcDVRCcH2b/aLGBu3lchOcoxpC0KMq1 XlF7WV8a/W/p7Na3b8c4oHwyt/kv+Lx+Y9xY9h38Gy+gVGTu+Sv3QjrpJlCOqFdwDoEv wi/M5NxUMO0YUqYiX32dYd8FHnlB0WdXyWtA2D+4b2RpqVHtEXir6COHZGbtDUh3WSmM C0ntfE/injH+iYrv5FXqnLS1PLAAe3a8Ryw1lgGKF7D/5S8BJZG9+rKHfCmFqpCa77Mq BpOQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=N+pwW9OX; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x134.google.com (mail-lf1-x134.google.com. [2a00:1450:4864:20::134]) by gmr-mx.google.com with ESMTPS id q11si4943528ljg.2.2019.08.07.15.13.53 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Wed, 07 Aug 2019 15:13:53 -0700 (PDT) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) client-ip=2a00:1450:4864:20::134; Received: by mail-lf1-x134.google.com with SMTP id b17so65221144lff.7 for ; Wed, 07 Aug 2019 15:13:53 -0700 (PDT) X-Received: by 2002:ac2:4d02:: with SMTP id r2mr6947720lfi.138.1565216033477; Wed, 07 Aug 2019 15:13:53 -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: Nicolai Kraus Date: Thu, 8 Aug 2019 00:13:41 +0200 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: =?UTF-8?B?0JLQsNC70LXRgNC40Lkg0JjRgdCw0LXQsg==?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000ac189b058f8e410e" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=N+pwW9OX; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) smtp.mailfrom=nicolai.kraus@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: , --000000000000ac189b058f8e410e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Exciting and impressive! Many of Arend's features sound very useful! I find the universes most interesting, but I don't understand how exactly they work. From your site, I learned: * A universe in Arend has two parameters, for size and for homotopy level. * Universes are cumulative in both parameters. Is type-checking still decidable? Say, we have this judgment: (1) A : \3-Type 1 We have (2) A : \4-Type 1 by cumulativity, but it shouldn't be decidable whether we also have (3) A : \2-Type 1. In book-HoTT, only (1) would type-check, since A would be a pair of a type and a proof of its homotopy level (i.e. you can only get (2,3) by changing the proof). But your site says these proofs don't need to be carried around. Are they still somewhere hidden in the background? On Wed, Aug 7, 2019 at 12:16 AM =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 mo= re > 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 an= d > class system. We believe that a theorem prover should be convenient to us= e. > 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 synt= ax > 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. Th= at 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-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/CA%2BAZBBpjRJ8ndS-jWaL-NT3HOtQ1S8nb_tefa6P13zkLcbZJPA%40= mail.gmail.com. --000000000000ac189b058f8e410e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Exciting and impressive! Many of Arend= 9;s features sound very useful!
I find the universes most interesting, b= ut I don't understand how exactly they work. From your site, I learned:=
* A universe in Arend has two parameters, for size and for homotopy lev= el.
* Universes are cumulative in both parameters.

Is type-checki= ng still decidable? Say, we have this judgment:
(1) =C2=A0A : \3-Type 1=
We have
(2) =C2=A0A : \4-Type 1
by cumulativity, but it shouldn&#= 39;t be decidable whether we also have
(3) =C2=A0A : \2-Type 1.
In bo= ok-HoTT, only (1) would type-check, since A would be a pair of a type and a= proof of its homotopy level (i.e. you can only get (2,3) by changing the p= roof). But your site says these proofs don't need to be carried around.= Are they still somewhere hidden in the background?



On Wed, Aug 7, 2019 at 12:16 AM =D0=92=D0= =B0=D0=BB=D0=B5=D1=80=D0=B8=D0=B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 <valery.isaev@gmail.com> wrote:
= Arend is a new theorem prover that have been developed at=C2=A0JetBrains=C2=A0for quite s= ome time. We are proud to announce that the first version of the language w= as released! To learn more about Arend, visit our=C2=A0site.

Arend = is based on a version of homotopy type theory that includes some of the cub= ical features. In particular, it has native higher inductive types, includi= ng higher inductive-inductive types. It also has other features which are n= ecessary for a theorem prover such as universe polymorphism and class syste= m. We believe that a theorem prover should be convenient to use. That is wh= y we also developed a plugin for=C2=A0IntelliJ IDEA=C2=A0that turns it into a full-f= ledged IDE for the Arend language. It implements many standard features suc= h as syntax highlighting, completion, auto import, and auto formatting. It = also has some language-specific features such as incremental typechecking a= nd various refactoring tools.

To learn more about = Arend, you can check out the=C2=A0documentation. You can also learn a lot= from studying the=C2=A0standard library. It implements some basic algebra, i= ncluding localization of rings, and homotopy theory, including joins, modal= ities, and localization of types.

Frequently asked= questions (that nobody asked):

--
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 ht= tps://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 &= 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/CA%2BAZBBpjRJ8ndS-jWaL-NT3HOtQ1= S8nb_tefa6P13zkLcbZJPA%40mail.gmail.com.
--000000000000ac189b058f8e410e--