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-wr1-x43a.google.com (mail-wr1-x43a.google.com [IPv6:2a00:1450:4864:20::43a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4189a974 for ; Thu, 8 Aug 2019 15:11:17 +0000 (UTC) Received: by mail-wr1-x43a.google.com with SMTP id x2sf45194293wru.22 for ; Thu, 08 Aug 2019 08:11:17 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565277077; cv=pass; d=google.com; s=arc-20160816; b=DJ/mX/3kW83cfrOwnF0GdvaeJBalBWcGcygCxktXNVaiQUyRvuLXHqHq9JYHBvcBnJ 58KHcxRC6JyjZGzHT3pEYgQEZf+pL3+2/eoLcYbIHTDLrbrWO1GO+d7YWlhx8X2wUShq 5XpUUyQq8dvJAWOkUCSgUVWogbgJWJrmJy4l8ZAKiOHhnOnIUv4fTCQgkn6YVMNWHTfo 9Y3lJliFWmekESDuCWP6hUbtPnVq+AvD4C3yESOwb7jxrdvXky/bzwGPX+2LdZVSJ3Dj a0d7MvJkRB0siQel5sjAXU7Va8g/R+LLBzrOkfCojV36fru0hHbxwEsoaIFXdixZMLm1 BXEQ== 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=KM3Hosh/TfoBj19sBtsyZi/G1c6KY4IkG8CkXdEAya0=; b=zR+xpTGXl8ScqI3eJ5Xt9qk+4xxrbKlNBT5uQNdBBMgTTDwr83a0zEbydggh7Y7qS/ Tv7mShk2cfI2XM4KjVHpkAm1d88xU1n2g7rLlBmD3CYItt+00PgvUQ/BTxOOQczzL6y1 EGF0rttKhzrVX9rqzJbtOjGRmNpDukWQzogdwYKyxBel5YswZlXMLOcmlURg3suU+f2U 6ntH/utzcprtnCPX1ZXYHpf2hwVC1JwChRKJVSYNHvdlPQ/8Wu2tFsKvAgCSFYni6ZcI h08QTnG9QRIWoFu+1VHMyQryhPW8hfDI91OVCbpGopkq9twdktGUR3cyZyS/Bm9iYZaF a4ZQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=UV1thUR+; spf=neutral (google.com: 64.147.123.20 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=KM3Hosh/TfoBj19sBtsyZi/G1c6KY4IkG8CkXdEAya0=; b=cWOW/VFktiDE324TGMibyXypfw2+U3+8INdglfi7do/8YVJLncPZKxxSchkJVJ6fvG dG2rYE0p+U3z1LaX/GX7LuyYk9SrHB/AyPCkSRBvHpObYX8PQk9HMZc0jl6sHsh3Aes/ 5I/vcvsyhvG2njqjWScUcpjpRXgh9A8n00EiqBmo/qlyEb5qSESNSWudDRCkCMw0We6j S5w5YN99TBGFVRlTaW73/601q07E4JpWb1K4bog5JP+GJSWZm66sf5G/c3BymDkblh8Y XABSh4dfzxhtcwYOhAr2Gm4A1EbDeX1SdmgDbUBEh2Xa2rapsVF7Ds0QTSRW1WdcDPfW Ngag== 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=KM3Hosh/TfoBj19sBtsyZi/G1c6KY4IkG8CkXdEAya0=; b=rJozeZ0Ibmm0h6bCYkieAappJh6UmePEN+BQWj1nBYqmCFl5yPfMmb2UvXxAXvnBo8 vit0JdlgbRmFBwpWZu+jaEZJbeSsqP/oFr+I1alFd7THZ72Xz519DmmU9wjVhLAdAOBJ oi0G09WBmn+ND1GJFftg+N0msRQV9M7xjXZ6Bq7bkwG8OOZnhLteQ83F5bHV/qocy43Y 5YoUYs9dqd3ZAxmzAxYU+BruZ5dMtr1n0ThkcvD46udbPiwaka+MVS6dG6zYXyshIJgY dfLiLsgTMsmfYjs+8VhI0ZpE/f0qObyBDs4RGYre/iXCqBcAnY/sMBIbhprEbqpPaYB6 i8Qg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVTz3hmAspnoJ+x5ZkUTK/LJT/DRkPXymyv0/g6Yh6Wc/IJQ43M C395i401baLDFsgPqXO3lwI= X-Google-Smtp-Source: APXvYqxuhheopzVGuoOwjO5WQUCzVuZ8fUllbH+1W9fGDRbnod16EjvOb35z614WYpgYRbXb7PWw6g== X-Received: by 2002:a05:600c:2182:: with SMTP id e2mr2608739wme.104.1565277076969; Thu, 08 Aug 2019 08:11:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:f78b:: with SMTP id q11ls18464729wrp.10.gmail; Thu, 08 Aug 2019 08:11:16 -0700 (PDT) X-Received: by 2002:a5d:6307:: with SMTP id i7mr4767052wru.144.1565277076230; Thu, 08 Aug 2019 08:11:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565277076; cv=none; d=google.com; s=arc-20160816; b=vcUyvnvGLIZmXnXAp52w1p0yZ7k1+FM3GdJrjvwkhUMDby7Q4/LjTKRlaU/hzb/Fi1 elY0fXDEyGAHp2yuUVoOV7MQjsnhvH1DlTlSjzyWdiYoN38qPqmAk8ET4j/3jFT+r72t WvPCyKPYFdtou7cI+k+k6OuvXOrXIMJrQEvc5YHJJgvQ7AxOsK1uRS5GL/GXxxpj15qX pzSiE8n/Rd3ZixHNm77UUhlC77oV1Dkv9dPX6BCIaCuAAhdEOAwXo5OwpqmuGglFrMsB nF9Yg7yLCdOIQXzm+FpuRWsMJZjPJKEGSalADkZEeUS6rCHjlPl7qDr/jbPuMr1TBvAn H4Ew== 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=a5iX6TSAJPveES0+SaRNPYYjo+NoWNMZEXgJsenFu4c=; b=jQT0OuiiSDpZIjodTBcnSmY5d1wrz8P7NnZt8aO7/Ayay5R2mNTU3rqMaeb6fFRv5M 8uGZelikUyDHxSgTGG0MMlgK0wT2b85zRrS5BnFYma7vlfs8k3a+R/KU6zyma47ofGU5 BXASR5gdh3rjUTge9xzBld4k3rVprDb3jkpYqesaeg60V2t+jOyqKCImKsaa0TV1d4KM pAtzAZmSbBCWd0NJrI0LO0rhRV5MV4MK7hIaHsh/u1kFC+kBVv9of3A88zBBv9csCNZK J9IPgbze2J6mKOaycGbLscVKmW7akCdq8GQQqXTrKSkwciYAelTM74hc2a+NBKR0jLuD cJmg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=UV1thUR+; spf=neutral (google.com: 64.147.123.20 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from wout4-smtp.messagingengine.com (wout4-smtp.messagingengine.com. [64.147.123.20]) by gmr-mx.google.com with ESMTPS id u18si5457817wri.5.2019.08.08.08.11.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 08:11:16 -0700 (PDT) Received-SPF: neutral (google.com: 64.147.123.20 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=64.147.123.20; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.west.internal (Postfix) with ESMTP id 4AB782A5 for ; Thu, 8 Aug 2019 11:11:14 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute2.internal (MEProxy); Thu, 08 Aug 2019 11:11:14 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduvddrudduhedgkeeiucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne goufhushhpvggtthffohhmrghinhculdegledmnecujfgurhepofgfggfkjghffffhvffu tgfgsehtqhertderreejnecuhfhrohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjoh hnsehjohhnmhhsthgvrhhlihhnghdrtghomheqnecuffhomhgrihhnpehjvghtsghrrghi nhhsrdgtohhmpdhtfihithhtvghrrdgtohhmpdhgohhoghhlvgdrtghomhdpghhithhhuh gsrdhiohdpghhithhhuhgsrdgtohhmnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjohhn sehjohhnmhhsthgvrhhlihhnghdrtghomhenucevlhhushhtvghrufhiiigvpedt X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 9C9505C0099; Thu, 8 Aug 2019 11:11:13 -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: In-Reply-To: References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> Date: Thu, 08 Aug 2019 11:11:12 -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=UV1thUR+; spf=neutral (google.com: 64.147.123.20 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: , 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-product axiom? = I apologize for my ignorance, model categories are not my area of expertise= . - In most models of HoTT that I'm familiar with, including simplicial sets = and several versions of cubical sets, the interval is not fibrant. What int= erpretation do have in mind for I? (btw, sorry if this has been discussed b= efore!). Thanks, Jon On Thu, Aug 8, 2019, at 10:45 AM, Valery Isaev wrote: > Yes, Arend implements the theory described in this document.=20 > Semantically, the additional constructions of this theory correspond to= =20 > the assumption that the model has a fibrant object I such that maps=20 > : X -> X \times I have the left lifting property with respect= =20 > to fibrations, and the path object functor is given by (-)^I. So, the=20 > usual interpretation in model categories (and other similar models) of=20 > HoTT extends to an interpretation of this theory if the model category=20 > is a Cartesian model category. >=20 > Regards, > Valery Isaev >=20 >=20 > =D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 15:29, Bas Spitte= rs : > > 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 > >=20 > > On Thu, Aug 8, 2019 at 2:20 PM Jon Sterling wro= te: > > > > > > Dear Valery, > > > > > > Arend looks really impressive, especially the IDE features! I look f= orward 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 som= ething 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 ty= pe theories. Is there any note or document that explains some of the mathem= atics 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 JetBrain= s > > > > for quite some time. We are proud to > > > > announce that the first version of the language was released! To l= earn > > > > 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 induc= tive > > > > types, including higher inductive-inductive types. It also has oth= er > > > > features which are necessary for a theorem prover such as universe > > > > polymorphism and class system. We believe that a theorem prover sh= ould > > > > 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 standa= rd > > > > 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 i= s 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 a= s 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 m= ore > > > > 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, a= nd > > > > 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 G= roups "Homotopy Type Theory" group. > > > To unsubscribe from this group and stop receiving emails from it, se= nd an email 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.fastma= il.com. > >=20 > > --=20 > > You received this message because you are subscribed to the Google Gro= ups "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/m= sgid/HomotopyTypeTheory/CAOoPQuSLoX8gKy54NQM6SNoi43wVA0A1Ad59qKs6prULkh6zBw= %40mail.gmail.com. >=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/CAA520ft6xBR1fJz4N0c= 5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.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/d0fd1d18-136b-41fa-b721-f64b9c487376%40www.fastmail.com.