From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a7b:c927:: with SMTP id h7mr4036230wml.122.1588340576331; Fri, 01 May 2020 06:42:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:438c:: with SMTP id i12ls5459307wrq.6.gmail; Fri, 01 May 2020 06:42:55 -0700 (PDT) X-Received: by 2002:adf:8b45:: with SMTP id v5mr4621588wra.175.1588340575139; Fri, 01 May 2020 06:42:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588340575; cv=none; d=google.com; s=arc-20160816; b=FtrqORvv4KldxYbAPxvYd905pKbMWMuqP33ElwEpb84i7b7VfIrR4TTGX3lZ4FCYMe Oz36WSblFj7AZyYdbl//ktn/egSe9f4xP3MF2kUMXfPmJLbisO07KLLZi9dUFJkP1RTP dqNjG0C+KoP7QuzUgt7cLTw+v8CbRTfeCb/OOSg8qPCWGYFBGciFoDwDlxuQQLkSeKrg ECzMKkYaX0mipaWMiVMt9tOMO1SlXVbrXXcuiBBcpVpHDVjTjaDy6253/uM2OeUGCc9o KaYmxfCOZSKRg6GSd7KM62kRt6hleX2aDuMyNikTFokb24yeY/oCO9ZBxReAT2pzylUW 9IjQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature; bh=eyqqlgsP3f2HG2BjBrTwkLpX0Guo63uoUqOqr7wADVY=; b=FuoAhmFOikobvkcoBXN6q5HkTjNGlFOG3L1aT4iRTTWzR1pAMHgPJggm5eQE1TiuZV LL9nDN4ZjJeOAP9QrFD1JYsF6ZayhN8TxyCzkAureLXFdGL7DSgiBh6N3Q7MYRKoEHu5 C7T5nNUy5Nmwmq0u7g1Dyi89FnUH5OMl2TBivtrkr7JWzKj+jQM7sywSMex5J+toCRja OgXVOtvMPS8qZFzzd4Rm14jzAyR1HRGf1irIORw8qujlMsRcceioFCMQmy36hTCn/qgo aM7MIyHNki5kbymG7PKpvSHX3XQdhT/NnVv6k2HWlBH1u3oJ5APm4BtTHFsHBvZxko8U duUg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=bMA11mK2; spf=pass (google.com: domain of dane...@gmail.com designates 2a00:1450:4864:20::435 as permitted sender) smtp.mailfrom=dane...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr1-x435.google.com (mail-wr1-x435.google.com. [2a00:1450:4864:20::435]) by gmr-mx.google.com with ESMTPS id q17si178180wmg.1.2020.05.01.06.42.55 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 01 May 2020 06:42:55 -0700 (PDT) Received-SPF: pass (google.com: domain of dane...@gmail.com designates 2a00:1450:4864:20::435 as permitted sender) client-ip=2a00:1450:4864:20::435; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=bMA11mK2; spf=pass (google.com: domain of dane...@gmail.com designates 2a00:1450:4864:20::435 as permitted sender) smtp.mailfrom=dane...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wr1-x435.google.com with SMTP id h9so1247214wrt.0 for ; Fri, 01 May 2020 06:42:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references; bh=eyqqlgsP3f2HG2BjBrTwkLpX0Guo63uoUqOqr7wADVY=; b=bMA11mK26/W3KhSmaHltzMphH8glxLh+o40OvwKEZtfeu4Im7N2W1bYcllEmFwwHxb GnHS+ZIFCW/xWcUnf7C4koex8DycIhD8j0OsK/bvQcctSTS9KfJDOQ3qoPQIldBWZjEV Hz4GyInP66P6c/8YNRthMx1pomGqfqoo+hATydahLr9MZ19ohoCT62/dzDUNJU2M4G0m jjRTSjPj/c8/rg3+Mz97bvd7tB83bYoHoOpRxPcGSfn/JKzlCzbr569JA1zJj23JvKTA WiapLeNDkBYWpZhtut21IxT3VINzx55p68sSm0waCHwo+JGVAVc8cPuN/mq8VMCDq4lI pphw== X-Gm-Message-State: AGi0PubKZkc/C/l2/YdRoy4RNXiAJCEOdEYmqFLcNdZI9b2Di3axIZzz R4XjOmzFQlAu3jU7y7Ent7oPYU0lLGM= X-Received: by 2002:adf:a18c:: with SMTP id u12mr4180951wru.325.1588340574913; Fri, 01 May 2020 06:42:54 -0700 (PDT) Return-Path: Received: from [192.168.1.148] (APN-123-247-156-gprs.simobil.net. [46.123.247.156]) by smtp.gmail.com with ESMTPSA id i17sm4416309wru.39.2020.05.01.06.42.53 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 May 2020 06:42:54 -0700 (PDT) From: Danel Ahman Message-Id: <600DEBDC-B1B6-4ED2-9D43-8009CD9FA94A@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_66E68E86-A177-499F-AB9E-4DEA2D68376C" Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.14\)) Subject: Re: [HoTT] Re: An online seminar about the Arend proof assistant Date: Fri, 1 May 2020 15:42:52 +0200 In-Reply-To: Cc: "HomotopyT...@googlegroups.com" To: Stefan Monnier References: X-Mailer: Apple Mail (2.3445.104.14) --Apple-Mail=_66E68E86-A177-499F-AB9E-4DEA2D68376C Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Yes it was, see https://vimeo.com/413726748 Danel > On 1 May 2020, at 15:41, Stefan Monnier wrote: >=20 >> Title: Arend proof assistant >> Time: Thursday, April 30, 2020 from 18:00 to 19:00 (Central European >> Summer Time, UTC+2) >> Location: online at Zoom ID 965 4439 5816 (https://zoom.us/j/96544395816= ) >> Speaker: Valery Isaev (JetBrains research) >=20 > I managed to miss it. Any chance it was recorded? >=20 >=20 > Stefan >=20 > --=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= email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/jwv4kszydtr.fsf-monnier%2BInbox%40gnu.org. --Apple-Mail=_66E68E86-A177-499F-AB9E-4DEA2D68376C Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii Yes it was, see https://vimeo.com/413726748=

Danel

On 1= May 2020, at 15:41, Stefan Monnier <mon...@iro.umontreal.ca> wrote:

Title: Arend proof assistant
Time: Thur= sday, April 30, 2020 from 18:00 to 19:00 (Central European
Su= mmer Time, UTC+2)
Location: online at Zoom ID 965 4439 5816 (= https://zoom.us/j/9654= 4395816)
Speaker: Valery Isaev (JetBrains research)

I managed to miss it.  Any chance= it was recorded?


  =      Stefan

--
You received this message because you are subscribed to the Google= Groups "Homotopy Type Theory" group.
To unsubscribe from thi= s group and stop receiving emails from it, send an email to HomotopyT...@googlegroups.com<= /a>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeT= heory/jwv4kszydtr.fsf-monnier%2BInbox%40gnu.org.

--Apple-Mail=_66E68E86-A177-499F-AB9E-4DEA2D68376C--