From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a5d:4712:: with SMTP id y18mr30604980wrq.306.1588029205386; Mon, 27 Apr 2020 16:13:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:5386:: with SMTP id d6ls25584645wrv.5.gmail; Mon, 27 Apr 2020 16:13:24 -0700 (PDT) X-Received: by 2002:adf:e58d:: with SMTP id l13mr31353899wrm.187.1588029204179; Mon, 27 Apr 2020 16:13:24 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588029204; cv=none; d=google.com; s=arc-20160816; b=tvkWA4NxqwgyG7fmLh3YDp1socghm/jWHGfZwNvcR8VvXUPpgArY3SqV58ZansVT6K KP6g7fpUZw6jxZiPH/31FKMa8dhZYol6VsiCIhFP4f6JswyCU7wKGJVHkkRcXo7NVNrW MhIM1Jt29ioWfXPFhoyJdVZiPCq5QKMyc+yxuBVFXtM5qy1XxtdSpqZcqA1qeJZwZcap eMV3nNJiW5DcwaAPd9WWi7UttNg4q2Ob2W9u1RVhV+PiWQY9aiDmp6v/WUQAH9DvSK5B V33NWEN2kgsR02QP/Kl8/QwZHY4uyqzH37YN+2fmv1tBMt9JAhIcmDagaBgo19nYYCR6 wFqw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=24CLKVoCQmMKLlJiMSp6fsItyJzxJQKxKDPdioZhzGg=; b=Vaaof6/GoYIZy2aI43WSh8eDfEXmLGYDHRDXJLiaZxIaxJYUeWrMp7OPN8UmcWWyw7 h336tpVsirD9LIwY0ZGUJMRi2hsGGS/0B0YBmEkDjHggqY5pqDLu9VCD419eeERzxxjp ca7U8b5993Zegl4agamJCo+zedvQWQzvBTs3qNcffdMzDnXDxlbAvzHVT9qQtQQXu/bG cRAc4a83tDcawcczB6U38cakJAYFqfkC2PkjiZ0sJVqj25cAK8J+r6ylZWL2qR337xjA s1U3lLl6lmAxUVPRy5Th1MM0RtWJv4kjigGvfEuq57A3YXzosjqVYgeoH4MpfCIfEjxz 8HBw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=jR4bBX2T; spf=neutral (google.com: 2a00:1450:4864:20::231 is neither permitted nor denied by best guess record for domain of andre...@andrej.com) smtp.mailfrom=andre...@andrej.com Return-Path: Received: from mail-lj1-x231.google.com (mail-lj1-x231.google.com. [2a00:1450:4864:20::231]) by gmr-mx.google.com with ESMTPS id x11si32145wmi.1.2020.04.27.16.13.24 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 27 Apr 2020 16:13:24 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4864:20::231 is neither permitted nor denied by best guess record for domain of andre...@andrej.com) client-ip=2a00:1450:4864:20::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=jR4bBX2T; spf=neutral (google.com: 2a00:1450:4864:20::231 is neither permitted nor denied by best guess record for domain of andre...@andrej.com) smtp.mailfrom=andre...@andrej.com Received: by mail-lj1-x231.google.com with SMTP id f18so19459673lja.13 for ; Mon, 27 Apr 2020 16:13:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:from:date:message-id:subject:to; bh=24CLKVoCQmMKLlJiMSp6fsItyJzxJQKxKDPdioZhzGg=; b=jR4bBX2TlpriILi6djCukpDJEcEOld34LTtKLwUi/2ZokXR1Bmd1EerV7lDyOJMKV6 5ekmM0FhgOEBaG6mRJG7fEWTyCVfePwORUAjAg/YfoFkvGTzzcwci/6gGQ9uVdbc4Gz7 EFhYMyocjL1mQiLxzuzJd3AsyfjLSun/qGEDSRBN/Q3eeL3JUhcSRTY2wgog3GPj8TY3 G7ouBhsT+yqxn0flOHZ+BEWei+bhGKhxp2b7v5oddSWHJIuiGrepSmRl79q9C0xhfAUh ZWUzEueWyAR2IQTsarJiBDFzTkopAVoouEiAY+MYsY/u2aPmldLkZMYSGufTugoi+Bvg XkBw== X-Gm-Message-State: AGi0Pub2u0KvH9kBjhuDDiwAeqOpV+eZTWSsLGqmCtIxRyHLjBkDkU2p zfbAJREjmaloMq/blxvou8bV7OBRg/2O1pUuBaUMbhObYRw= X-Received: by 2002:a2e:9255:: with SMTP id v21mr15776862ljg.222.1588029203171; Mon, 27 Apr 2020 16:13:23 -0700 (PDT) MIME-Version: 1.0 From: Andrej Bauer Date: Tue, 28 Apr 2020 01:13:07 +0200 Message-ID: Subject: An online seminar about the Arend proof assistant To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Dear all, I would like to draw your attention to an online seminar about the Arend proof assistant, which will be given by Valery Isaev. Title: Arend proof assistant Time: Thursday, April 30, 2020 from 19:00 to 20:00 (Central European Time) Location: online at Zoom ID 965 4439 5816 (https://zoom.us/j/96544395816) Speaker: Valery Isaev (JetBrains research) Abstract: I will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with convenient pattern matching principles for them. We also recently implemented a tactic framework which can be used to automate routine proofs and implement various EDSLs. Homotopic features of Arend include built-in universes of finite homotopy level, higher inductive types, univalence, and path types in the style of cubical type theories. I will talk about these features and also about our plans to implement language extensions that can be used to simplify reasoning about various higher structures. The seminar is the first one in a series of seminars about proof assistants, see my blog post http://math.andrej.com/2020/04/28/every-theorem-prover/ With kind regards, Andrej