From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:cf02:: with SMTP id j2mr4224676pgg.130.1588340566807; Fri, 01 May 2020 06:42:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:fe52:: with SMTP id x18ls6450048pgj.6.gmail; Fri, 01 May 2020 06:42:45 -0700 (PDT) X-Received: by 2002:a62:1452:: with SMTP id 79mr4215762pfu.108.1588340565143; Fri, 01 May 2020 06:42:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588340565; cv=none; d=google.com; s=arc-20160816; b=msCJI5ckNGUHrr3iDSQF/gB2v2Qet2F50VzzJoLG6F9IqutFov+h12TdJti6Hbk/XV ErppL4SKCLGcK4WSYrRk26r9gfR0+psHkOwLqgBoq2+6SeS7mf79F4eMAnD7jKdBizov Ya7W2O7L/Lgd5W5f86COxvUUL6F28sby8K1+FPH0zUYEYmgBm2eNnHo1NJyl8aVBxanf wBB84mf/SoPIl3z9YYMKKfepXTdHU6iWDpZvuH4xj+AE1ynTZmvCxHR6iKgMZfdDsns0 XsmMjiDYj5JCBAmBpMHOBB+o65l3FfJMr/PBVgh647Rcb2CB9FIhcyCnT480uYnx5kk0 NqUg== 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=k6r4kvpgVGhNAe85scZdH06DTwCxM7Wox5wvREHW3SM=; b=yU08i23qm3Irl8oyTjOQN97UtTGuixAqZ0EBdIx3993j0U46Uo92hml6mil5d4jyPW rdQmicUHiucg5ilcx3tSZcc3ElxpBn5f/IKGW30LW3OCA5TqVBj4+RcWmt5LIqG9UPTB g8zdYJjMPzeMr3x00yNuHaf+rSKhNSOOcyhwBujEaoGkM5I/ohdRhUuK4AYd2y2kJ2MA tMOU6dx9h8rJqaa0TAGzkdRPT6kWOz1yRFiYuAVmqXToVXRZNN7x8AlKL/LPB2Z9ROaA XuBSlCm+epqRNWrbteeQ55f8burBT8jyngU58F/XYnA1b7XzS0Emno8Kj6CvVWIzjvd4 WIUA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=RYsWkUx1; spf=pass (google.com: domain of anja.p...@gmail.com designates 2607:f8b0:4864:20::a34 as permitted sender) smtp.mailfrom=anja.p...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk1-xa34.google.com (mail-vk1-xa34.google.com. [2607:f8b0:4864:20::a34]) by gmr-mx.google.com with ESMTPS id q34si159866pjh.2.2020.05.01.06.42.45 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 01 May 2020 06:42:45 -0700 (PDT) Received-SPF: pass (google.com: domain of anja.p...@gmail.com designates 2607:f8b0:4864:20::a34 as permitted sender) client-ip=2607:f8b0:4864:20::a34; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=RYsWkUx1; spf=pass (google.com: domain of anja.p...@gmail.com designates 2607:f8b0:4864:20::a34 as permitted sender) smtp.mailfrom=anja.p...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vk1-xa34.google.com with SMTP id w68so2694210vke.5 for ; Fri, 01 May 2020 06:42:45 -0700 (PDT) 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; bh=k6r4kvpgVGhNAe85scZdH06DTwCxM7Wox5wvREHW3SM=; b=RYsWkUx1IrAXczNCtFW27ORNEwVHwdwnjlAibKrXl/Y1rP+ZM420GOzDQUGjy9v6we VmA8YvrYEQYHYIATqvUBMAyYbSyKb8zKsHxar3AxA+cIUomrVjcoReFG6bBJCvhJrxML bMv0ZnIMVo7dKS5SWWwPoQiTNpeBnt++h8CwAV+Dxb8Q7URU58htNbptVJh0xHAj6zlO q+cxJrcRRdxWC92u6/BAqaQGoWKHgeON9OiGgX/JNSH3hbpiD+CaIZWYMjJZTk/3ZmQF 4s2lJIgtOKGJMYROHWQWY6ClTh2z0OZsMHrAUDnKAc/Jy8y9m0CNKHG8lo1RY1JCOP7I zhzA== X-Gm-Message-State: AGi0PualmlpjMymzdrReOKvbyvB2zV2o9x4qYYIOV41BtZhk/u9eeise JaAppNsSxYrdmzHcKnNBdEypXUZtKfOd/2pF+gEqZg== X-Received: by 2002:a1f:2803:: with SMTP id o3mr2807752vko.28.1588340564234; Fri, 01 May 2020 06:42:44 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: =?UTF-8?Q?Anja_Petkovi=C4=87?= Date: Fri, 1 May 2020 15:42:33 +0200 Message-ID: Subject: Re: [HoTT] Re: An online seminar about the Arend proof assistant To: Stefan Monnier Cc: Andrej Bauer , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="0000000000001d14b305a4965b50" --0000000000001d14b305a4965b50 Content-Type: text/plain; charset="UTF-8" Indeed it was: https://vimeo.com/413726748 V pet., 1. maj 2020 15:41 je oseba Stefan Monnier napisala: > > 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) > > 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 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/msgid/HomotopyTypeTheory/jwv4kszydtr.fsf-monnier%2BInbox%40gnu.org > . > --0000000000001d14b305a4965b50 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Indeed it was:=C2=A0https://vimeo.com/413726748

V pet., 1. maj 2020 15:41 je oseba Stefan= Monnier <mon...@iro.umontrea= l.ca> napisala:
> 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)

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


=C2=A0 =C2=A0 =C2=A0 =C2=A0 Stefan

--
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 HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/m= sgid/HomotopyTypeTheory/jwv4kszydtr.fsf-monnier%2BInbox%40gnu.org.
--0000000000001d14b305a4965b50--