From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.5 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 8583 invoked from network); 11 Sep 2020 06:33:11 -0000 Received: from mail-pg1-x53d.google.com (2607:f8b0:4864:20::53d) by inbox.vuxu.org with ESMTPUTF8; 11 Sep 2020 06:33:11 -0000 Received: by mail-pg1-x53d.google.com with SMTP id a184sf5431679pgc.16 for ; Thu, 10 Sep 2020 23:33:11 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1599805986; cv=pass; d=google.com; s=arc-20160816; b=i6cCaq+TVTkpF/pSHmnNwSoPbxtMh7aX1jwKYjmELkmOPVbSHJLucEx+tbucj6uoQl jxenXlu4wVxA28ynwa/RfdkbeGKrQivXwvvWF72pKmAs0dS+B6VWAGc4dgOwD0/ds4w6 O0H1oqsBD+NeubsKvH5SYE8uy/LD6Ka0ZGaznc6+ru5mDjtQmrVzOVFmkLbn3MIl1/mw VSFGeUroq4A6v1n1KpquWMIvldC4tb4tFod/dAe9aSFOzPo1Fko+B5/oilZeGXIO5U1n j2/dXhP8p4QTD7EqO6RDRpbZYU/LjlhyiKRr8POcXluig2Fo5uXol4aZe6kuIoNzygvv D8+w== 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:to:subject :message-id:date:from:mime-version:sender:dkim-signature; bh=zSx51TTstiVUpiIMkuqz1l91T7vPwPLRkQjvmsES230=; b=sqh0s7d/HZOTHHFHxlzfWAG/BvBl29OdhMUVQfdjXDHGWeTQHLRbEetbQEq15f4vhj YxWmuH6b+iqShrR/sl+u2L2fqKknnuTbR4IkbEXEVGft7DWaP5cr+yke5O5OKkEGWVHG n1A4GXPJv9WLCJh8oPY5WDRj0nXWRSJbN24CLmwDT7GG3RYZjXcJj7ld1VLle0OhaYjE JYcRA9ql5aLuWpYODMPoB/l8/eJ5pwFjV69DiBvlGGiKyZUWiNC9h3+MnqxS6oP8zSXQ tPNE16loolaQpY5UzMPJ/1GfYoiYidySf5xoIk6T+v48Iatf0SkS+WFzZGc+5zdhZmKN 4j0A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=eKh304L9; spf=neutral (google.com: 2607:f8b0:4864:20::42c is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=zSx51TTstiVUpiIMkuqz1l91T7vPwPLRkQjvmsES230=; b=KSHpuMYy6FFPJY74COCtgR69NHBkuPVKv07lLPTctLqss4I0c30wJtGLvhhPzBPM+g /ictvkuuKdsU1EOXEeOgVOyydpXsK57Rli+nXTgyEzwAkqaJQt6AFNrYsA0NL95x5MiW TI2bOiOD9stz4JfsbvvbQJjSX+Lv/71YLBX6RqOVNagwzVBNQsInL1NkHKzHTo8GEJvN LHe8RRC3pe/kcqM2IpfWcZocyYvZoq7Dm6xs4V/lQGNSa4s9Jpr2UwEKp97zcjer9zeQ Y8I671c0GQQ70TycrOOGPj33rshwpR3uxxGvN+Ig8bfTfrI9fPA6eLxor2lxuf9mABCh cPhA== 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:from:date:message-id:subject :to: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=zSx51TTstiVUpiIMkuqz1l91T7vPwPLRkQjvmsES230=; b=Glwan4HbuHi18FcI48byoVHMfn72ufr9OH1UM5zptQg8nyMvL6GPsHpUp2qglHI1lp uaZ46mbsP1KcN7nX/4uytfklxaQBtCrOrcFcghEOcc73kk00xEYxtmeRVhKXlxCkCZBp bAacY5Rk1BbsHbAWyyEFxRNmADdORIkI7ryps/+h6tc+swG32lzzRGBo+CWgU3pdwemO TgNKWLNPM+x335T6dzm1bOy7+gNFOwUyFHAgMjyg6h4sa0rPwO7RLDzxpuv711YdDuBY kIA3gIAEEz75ZeEJR9V5YcxsNzpPZnJZs6GIdv1zM7aIA/8OhBtVOAK/E3nmq6mkCROW /7ow== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533X3OP0UiAvXj0mVtLTbzG9WlqNuPdatAvtj2Yn95YzP3Fvdyxw JceRyTEWPdM/c24jp+COZ0Q= X-Google-Smtp-Source: ABdhPJxS+u0NymhdK0jO8b5mwMzG9i4aGp7sWpERQOyliSc+/q6dQcvMfdkcJMzFo3PB2vcPwAXQ5Q== X-Received: by 2002:a17:902:b70e:: with SMTP id d14mr560608pls.15.1599805985786; Thu, 10 Sep 2020 23:33:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:79c6:: with SMTP id u189ls424222pgc.9.gmail; Thu, 10 Sep 2020 23:33:05 -0700 (PDT) X-Received: by 2002:aa7:961b:0:b029:13e:d13d:a082 with SMTP id q27-20020aa7961b0000b029013ed13da082mr849085pfg.25.1599805985168; Thu, 10 Sep 2020 23:33:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1599805985; cv=none; d=google.com; s=arc-20160816; b=dEa4D+4Jvf9POAk/oBjnnx8l+WeSHHSuQUwzg08gmBoRG9JYi+wtabKLr6WOzmJ/0u 48MaRLxuk9sDntKNm7/bdYRi0Hfo3rM+aNgz5LurFoe10m8oGmN/zCLtgVeHDone+uLF WjF2ZoKH5Apcv9hGqi7sH2uhLrVDYRdpIIfHRx66xeDTWT+GkTLoKgfxGU/5PxfGJo0z DLfABuodAbp6DqBcXLpPdF7fvE9v6mmqKg4/XmD742nSF+Dyc6S/M5EUzIC2GE571Ce7 iSFK6+hh7y/vioS0ewChUIxzZwfwoZYhsT6DrCihnzvsbfAUH8B58K7s3aYh8uasfF2v K/uQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=615Gm1Bz+qQUT9arl7+xB5KrZleaE48cEK0u0kTV8G4=; b=Y8sOK40ZT0r8r4P6PvnvFuwk7gf4JKhDNRbSqqP4NAzW0nUNmbosZuPSY3VU1i2D4k qyp6+AAF2QoXxZSJtF/j0edOFIneCeWx9Qw4+bGGTz+3qqCZD4QmrH/lL4r61z05olZo nmKFBNVq2m6tLTc/XKSnnBmEfnU3+xPkg2T4SCRHjiAnVykFhu32Xmb2qtA5uAXP8FVC Bvq62GMkHyYxqmo5pM5mMstejpwvKPDNUkp9VmR4wTeEOMyixVQfK99BNek702WvXIyD j32zbBJN7DNuxD0aVdWmb493MyK7pNeqVkzWPWaiABj3GRgxwtytVYkyCmJCdVLnN0nv mg7Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=eKh304L9; spf=neutral (google.com: 2607:f8b0:4864:20::42c is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com Received: from mail-pf1-x42c.google.com (mail-pf1-x42c.google.com. [2607:f8b0:4864:20::42c]) by gmr-mx.google.com with ESMTPS id d60si415478pjk.0.2020.09.10.23.33.04 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 10 Sep 2020 23:33:04 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::42c is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) client-ip=2607:f8b0:4864:20::42c; Received: by mail-pf1-x42c.google.com with SMTP id w7so6527142pfi.4 for ; Thu, 10 Sep 2020 23:33:04 -0700 (PDT) X-Received: by 2002:a63:485c:: with SMTP id x28mr627431pgk.289.1599805983772; Thu, 10 Sep 2020 23:33:03 -0700 (PDT) MIME-Version: 1.0 From: Andrej Bauer Date: Fri, 11 Sep 2020 08:32:48 +0200 Message-ID: Subject: [HoTT] Every proof assistant seminar series: Cubical Agda (September 17, 2022) To: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=eKh304L9; spf=neutral (google.com: 2607:f8b0:4864:20::42c is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.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: , It is my pleasure to announce the next talk in the Every proof assistant on-line seminar series. We are starting the Fall season with Anders M=C3=B6rtberg who will talk about Cubical Agda. With kind regards, Andrej CUBICAL AGDA: A DEPENDENTLY TYPED PROGRAMMING LANGUAGE WITH UNIVALENCE AND HIGHER INDUCTIVE TYPES Anders M=C3=B6rtberg Stockholm University Thursday, September 17, 2020 15:00 to 16:00 (Central European Summer Time, UTC+2) Location: online at Zoom ID 989 0478 8985, https://zoom.us/j/98904788985 Proof assistant: Cubical Agda, https://github.com/agda/cubical Abstract: The dependently typed programming language Agda has recently been extended with a cubical mode which provides extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically to proof assistants based on dependent type theory which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. In the talk I will discuss how Agda was extended to a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. I will also show a variety of examples of how to use Cubical Agda in practice to reason about mathematics and computer science. --=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/CAB0nkh1qFFEtkb90aj7RBy%2Bf407nJRwjLdWcu8BvMC1N6Z3c7A%40= mail.gmail.com.