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-pf1-x43a.google.com (mail-pf1-x43a.google.com [IPv6:2607:f8b0:4864:20::43a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f654d139 for ; Thu, 8 Aug 2019 09:56:26 +0000 (UTC) Received: by mail-pf1-x43a.google.com with SMTP id 191sf58759112pfy.20 for ; Thu, 08 Aug 2019 02:56:25 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565258184; cv=pass; d=google.com; s=arc-20160816; b=ZEBafaSozR2nKKgBVWhKzOQo1QvzRHEqySh02/qggjVuRjDIMgtDck1tmk4+KSqOcx 8Oy1oYpOCun//nkeJn0DsU1A7Ee4jSGnBo2wW3IEmJqRyXcPvgcqK0JwPRrUESPYigdU HhF4gAOYF6VxPMASCOilsNM7UCodRQU5UjjF7FGhl3ltlUQk15C1sOgJvJuHKWhWRhgJ oAQ2eagDgEqxMaeSf+1x13M/vEVMIg3zeiE7paeM2eFwvC2Da7OQe6WBrpFoBz6j6eYP 44G1rF/FyBlw0meIRq0HYMD/63k0n4eislGytcTKSKe3NNUcyBvpAMveMtNJbqiVYnle ksTA== 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=/lwbsSb76fSRWcLkdawVSoEqGQxIjeRSroTy//ICXOk=; b=b0sSW8130e6Uy31ARCIPY4NjhXGF4YAapXpI9p+9gMs2LiYGGb8pjUKoyGS9j55bMJ hBK/7wFrFS6tvYu+rv7lLrHRQ+Mcmkl/8aVPyDigI8Kw2axEggvxlaf4j3XsXaYLDw6v 5xK59zLkKmqRhmci8m901cZyJ3AvXJSnINRzgsP8jEXhaEgLfIYepv9643OlWEZNy9UW YlhxmZ5vyiagOyfVGDfanhLjRdTpHaVvVKmmcYaPCdRp5RBkhgq7UEG+34GmTsiRztDX GXu5fmxSqaQPWZubP9yMnUgnlazS471zcPwtBxVlgsIpcKjngIWphWLydcLTIjwXi6t6 HCxA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="e8hRTlf/"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32b 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=/lwbsSb76fSRWcLkdawVSoEqGQxIjeRSroTy//ICXOk=; b=nNtBMdIkOA+lxAymfhRaV7xKRG4v6k7138nY/d6FqE4FcJS1fzc9WmA/Kow9Mb+Fsd CogORV1j81sHET5g60TcmFOm9Rs50QoUm74JRP9BTbkyeDd2B4j6RouSwIFi+91/6wfX CsjSFjG4/kvi8PgcQmPCk2NzZRvNSUtrR1WQMuO6zkB3xJS1r6QSRPaZ4Mjf4S/Jsw5K lX9qaY9DWT3zMdTR/KDcWmtuvGSyBChl/NNFyJu3rIOEnOH3kdQSNqe7e+GyWGOa2EYZ 75WgPQYBJow7P193oeazQ9a5R77tZu1j51/YHFlad+wsCSN+foXHPLs/fU+Jw/+2gqMi C9QQ== 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=/lwbsSb76fSRWcLkdawVSoEqGQxIjeRSroTy//ICXOk=; b=c7z2E8WlxSrJ47Iwi0sesbcY43khso6CdiZgJTDWOqbN5X2zmIbG+jVmRR+cTe/737 fz2N8AxkTFQgQpR/u0PHEHFGpc9EXi+Uo7RT+e4r25DdR/EYne5849Qjj5mlpgaUkuVa +lE8uaQMDuPlSV2DZB6+AyOMJtoOOEXuqkmvGHt7D3moJ033ItSbNgIJpY5lDRqAipUt pDumB7BVgrHltOyWVZENKM9fBAYXeQ6yJ/HTy6DgmAmH1l8VodRItHuCfSNTd36DKiUY 8vhWg/r302ILVRcBQ05FV7js8Tl6fKc5wcxuwL1lv17zKZ/7/4lQIBxG3GDvpLvHZbwO Fyfg== 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=/lwbsSb76fSRWcLkdawVSoEqGQxIjeRSroTy//ICXOk=; b=hE+AAjlm+rVAu1rZKmH4bo3EKX8xHGaQ1gheKc+G9bksOUzZ5dk18998JEwCq5YzW2 QJkZayzfxuewCLNgYFcmToAoMh4UtecIuzHlQWujPeYvZEu6ACxANT4LcVMSLphEB+U2 rCv/f2wDXx99c0DCcXVQFc1mZa4RaA/C+/3TVpRPGyzO8nz3BqgzFAWpXbHkqT21T5Jm 4cweNnPKEqkTVX5gh/TO40tLkfnt/CXBlzCgCrIbpMzsq0AYG2FfMjHDTpDhBsr5v5TC lUPAhhm0PTv8Zg2EGGbb+IGupQXsTSYNWg/eohAXKfNjbmVAv5Ky8JtO/BJ+svypPLuW wFcQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXwyUfJmrgmBTBAhdemwf2PQwK868zqngzQHoErbqPgQYKTqqho +Di0iskwFbIzK6oCaDiYZeg= X-Google-Smtp-Source: APXvYqy0FJ/5TNpy1gOKjFdAY4rZz7bhoRMBEUZGRwpLAzf8FpKEWqYIjJhcZivCC3PvwZQ+mFteOA== X-Received: by 2002:aa7:8711:: with SMTP id b17mr14756715pfo.234.1565258183734; Thu, 08 Aug 2019 02:56:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:3043:: with SMTP id w64ls20572345pgw.15.gmail; Thu, 08 Aug 2019 02:56:23 -0700 (PDT) X-Received: by 2002:a62:483:: with SMTP id 125mr14956141pfe.245.1565258183308; Thu, 08 Aug 2019 02:56:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565258183; cv=none; d=google.com; s=arc-20160816; b=R8goofXwrMlc/fOkltlm475I7FJC1q+GzxMdjblMCx8dcIr/ujIG6eSALnsfn4/7+4 RU/t2fpUa2TdHnFqvn5kfh8cGYj5Ura3duCZeWpXwh2Es4rJlKcJs47hVFASmpMwq+KU pli/rGSg2ZS0qxR4LWn25F8BEacCAZv3gBD8FZ5esyNX2Ui87Q1bgsl1BP6YfgzlQYsT 4WAfSpdPzAc6exWKGVzagM8/Ct+xrz/sWc+/CrjaS9/6bFLFOosvaAAM2PSQou/mHU1Q reL3l/MejGEIO89QMCdPhqHnC/gfc04YB4x/uT8HtpHtTHeZpx64L4ijqZ5qpu5X24Ro J+Dg== 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=3cD7dqtitLKy1SN4ml5H6F9K3GNRznc+td/9LbLt0y8=; b=TKs9za526MYMJSreHXrfN+GOPZi4l4IVU2yia41k+/ViTJ5E3tb0/uRz36acH01c6W Fac0KhgmG8tkaisSnaF8hm7xVgKd4D/KjIz+fm+5HEvFXCRqmXcbKneODJO6WD7Y6Qq8 DGJsPANNsUan1dngqN9v4nME6esgSiCMQJ+h06/l1eUHG28AfIw7hC8VNUnlUwKHGc4E o0fyH8Cm+zCvfM2d/rs3GbHFJqgDAGBD32WD221Ry7kS93ed5WtvLDzYM5LN9BvH0CLr Na+BIL+5hv6Q9WiceVXLkQhTqd1tDhIBV9ZHAmeWGKaZXrxMFW/p6wn40ToSmtTrKno8 7viQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="e8hRTlf/"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32b 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-x32b.google.com (mail-ot1-x32b.google.com. [2607:f8b0:4864:20::32b]) by gmr-mx.google.com with ESMTPS id h14si4395041plr.2.2019.08.08.02.56.23 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 02:56:23 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32b as permitted sender) client-ip=2607:f8b0:4864:20::32b; Received: by mail-ot1-x32b.google.com with SMTP id x21so22895797otq.12 for ; Thu, 08 Aug 2019 02:56:23 -0700 (PDT) X-Received: by 2002:a5d:8253:: with SMTP id n19mr3505076ioo.80.1565258182930; Thu, 08 Aug 2019 02:56:22 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> In-Reply-To: From: Valery Isaev Date: Thu, 8 Aug 2019 12:55:46 +0300 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Nicolai Kraus Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000f9b995058f98115e" 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="e8hRTlf/"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32b 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: , --000000000000f9b995058f98115e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable You can say that they are hidden in the background, but I prefer to think about this in a different way. I think about \Set0 as a *strict* subtype of \Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) is only homotopically embeds into \Type0. It is equivalent to \Set0, but not isomorphic to it. In particular, this means that every type in \Set0 satisfies isSet and every type in \Type0 which satisfies isSet is equivalent to some type in \Set0, but not necessarily belongs to \Set0 itself. So, if we have (1), we also have (2) and we do not have (3). It may be true that A is a 2-type, which means that there is a type A' : \2-Type 1 equivalent to A, but A itself does not belong to \2-Type 1. Regards, Valery Isaev =D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 01:13, Nicolai Krau= s : > 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 typ= e > and a proof of its homotopy level (i.e. you can only get (2,3) by changin= g > 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 m= ore >> about Arend, visit our site . >> >> Arend is based on a version of homotopy type theory that includes some o= f >> the cubical features. In particular, it has native higher inductive type= s, >> including higher inductive-inductive types. It also has other features >> which are necessary for a theorem prover such as universe polymorphism a= nd >> class system. We believe that a theorem prover should be convenient to u= se. >> 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 syn= tax >> 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 w= e >> implemented IntelliJ Arend >> . This also >> means that the underlying theory should be powerful and expressive. T= hat is >> why Arend is based on homotopy type theory and has features such as a= n >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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 >> >> . >> > --=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/CAA520fsVx%2BGUpYN%2ByPesJ_1PwKV0MfU%3DGQD4ovpfHhy%3DDuj= 7yA%40mail.gmail.com. --000000000000f9b995058f98115e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
You can say that they are hidden in the background, b= ut I prefer to think about this in a different way. I think about \Set0 as = a strict=C2=A0subtype of \Type0. In comparison, the type \Sigma (A := \Type0) (isSet A) is only homotopically embeds into \Type0. It is equivale= nt to \Set0, but not isomorphic to it. In particular, this means that every= type in \Set0 satisfies isSet and every type in \Type0 which satisfies isS= et is equivalent to some type in \Set0, but not=C2=A0necessarily belongs to= \Set0 itself. So, if we have (1), we also have (2) and we do not have (3).= It may be true that A is a 2-type, which means that there is a type A'= : \2-Type 1 equivalent to A, but A itself does not belong to \2-Type 1.
Regards,
Valery Isaev
<= /div>

=D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 01:13, Nicolai K= raus <nicol= ai.kraus@gmail.com>:
Exciting and impressive! Many= of Arend's features sound very useful!
I find the universes most in= teresting, 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) =C2=A0A= : \3-Type 1
We have
(2) =C2=A0A : \4-Type 1
by cumulativity, but = it shouldn't be decidable whether we also have
(3) =C2=A0A : \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 ch= anging the proof). But your site says these proofs don't need to be car= ried 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 bee= n developed at=C2=A0JetBrains=C2=A0for quite some time. We are proud to announce that the= first version of the language was released! To learn more about Arend, vis= it our=C2=A0sit= e.

Arend is based on a version of homotopy type theo= ry that includes some of the cubical features. In particular, it has native= higher inductive types, including higher inductive-inductive types. It als= o has other features which are necessary for a theorem prover such as unive= rse polymorphism and class system. We believe that a theorem prover should = be convenient to use. That is why we also developed a plugin for=C2=A0IntelliJ IDEA= =C2=A0that turns it into a full-fledged IDE for the Arend language. It impl= ements many standard features such as syntax highlighting, completion, auto= import, and auto formatting. It also has some language-specific features s= uch as incremental typechecking and various refactoring tools.
To learn more about Arend, you can check out the=C2=A0documenta= tion. You can also learn a lot from studying the=C2=A0standard library. I= t implements some basic algebra, including localization of rings, and homot= opy 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 p= rover should be convenient to use. This means that it should have an IDE co= mparable to that of mainstream programming languages. That is why we implem= ented=C2=A0IntelliJ Arend. This also means that the underlying = theory should be powerful and expressive. That is why Arend is based on hom= otopy type theory and has features such as an impredicative type of proposi= tions 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, bu= t it computes more terms than ordinary homotopy type theory, which makes it= more convenient in many aspects.
If you want to know about l= anguage updates, you can follow us on=C2=A0twitter. Questions, suggestions, and commen= ts are welcome at=C2=A0google groups.

--
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 htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520fsVx%2BGUpYN%2ByPes= J_1PwKV0MfU%3DGQD4ovpfHhy%3DDuj7yA%40mail.gmail.com.
--000000000000f9b995058f98115e--