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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6191bc4f for ; Fri, 9 Nov 2018 07:38:54 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id j15sf603886ota.17 for ; Thu, 08 Nov 2018 23:38:53 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=5SoOzYkOKvGYYaTPNqDhJFFm2MsxnU/bcR2JeKS9dq4=; b=QyIc+CHJ4+X+kQ++MR1wsmEl0R+7rnruJ1tgKYpy8fTiI+senqWFmHMkEE7BvEIRkr 2fyie4etFkfI18BUmOoGyQ246Rzz7y16/DLfAKVApDrHI4edVpc17dzsQE3F4y7fAnGq AI0saEW4/SkyJDI/qocIN3d6sqgLGN0Q+NEiDRawUjACey7VThwEpJLoM9U9PYV7SxRb g3Rc+HH/nRM42snloGMrYxAAb+rbG8pQgsLCxKxNzhg64Si9PPnlFOHsBMIBPTM/nRPK KUj00w9hjZNHDna34y9LorVcapPWNCXmJ60rvrz5KNEqCJvGYtZeLc9o4lAb12S1snV6 6n3w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=5SoOzYkOKvGYYaTPNqDhJFFm2MsxnU/bcR2JeKS9dq4=; b=dpmL9Xn4YPOMOGXy8GXc87Jh8RjSG3Xn714GZxoOaelVaVvkooOxTGuNDEU0IPqB7l rRJ/IpOspVekdDjCffkQkdaLtfYtm9fJ+Gtr976zAXwe85Vi84CjCcBXRq9OXDAGyBmT kmirxx4s/+Ph2VO9UCCB8CJRmri3+KbcJAPlae5LB7qfukUZe0+jAItsr+1O3sZM/vFj SC8Rjt0Soi5/CNhPKTgHeggjE3VYW/ry5vWqs9DXwpdlT/wRd8Ip9ujG+MfCs692pXXA ePHjWKzsBQmI4FTc3owBWsMM9Cv5La2KWsztqnTDMpORrNtmFrdsqEfW0rGjLz/z3b/e xI5w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=5SoOzYkOKvGYYaTPNqDhJFFm2MsxnU/bcR2JeKS9dq4=; b=d9LDaviFfPSQnQSAav7QkfTgL1DOTufPnk0kS+YVe1ElGZDAmY4uF0g22U0eyEmxb1 TT470wGf1ZnGWsmoHi7z1X8IyKjitzT7RqDUdi7wk+IM61Z7yFk3MURJxAdNUGciUK2W zoGVPYg+meSQNYUNZdPzSOHpmyak6nXXsaFXC3gKACSchTgKhlc4njO0xvjfiEW1g6wu gE5Ct104R/XOnUleWyoKy+bMCupUcMFGRc4uEEfKFLNZLsT2kmYlnIQkTmSPIUI5iD86 Zjzq9g633PLFRHsFY51V28ma2DtGvoGOLWsMmnT/YaMiGCa3rPRMmj1U3cF8X7wmjW3m aEoA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKAyjKk7LkXTd9XEWNuUWniMgywuq31u6gf/WaNNzLPSjtajV0O +zFndbgBAeGrNAiRdlq/G4Q= X-Google-Smtp-Source: AJdET5c5D7ChpOMLlsyFJknlakLsR9He4MMNe9ZvpZm9L4XgwtYkg6cFSiNRJ8IYV4kUH3kmdiiKEg== X-Received: by 2002:aca:37c1:: with SMTP id e184-v6mr81917oia.5.1541749132905; Thu, 08 Nov 2018 23:38:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5e8e:: with SMTP id f14ls441984otl.2.gmail; Thu, 08 Nov 2018 23:38:52 -0800 (PST) X-Received: by 2002:a9d:fed:: with SMTP id m42mr129649otd.6.1541749132357; Thu, 08 Nov 2018 23:38:52 -0800 (PST) Date: Thu, 8 Nov 2018 23:38:51 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: In-Reply-To: <8a0d0d80-2ee6-471d-b5e6-f9aefdc7b7af@googlegroups.com> References: <8a0d0d80-2ee6-471d-b5e6-f9aefdc7b7af@googlegroups.com> Subject: [HoTT] Re: Computer-generated proofs for the monoidal structure of the smash product MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_856_1310116136.1541749131790" X-Original-Sender: alizter@gmail.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: , ------=_Part_856_1310116136.1541749131790 Content-Type: multipart/alternative; boundary="----=_Part_857_1066256179.1541749131790" ------=_Part_857_1066256179.1541749131790 Content-Type: text/plain; charset="UTF-8" Here are the slides: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Brunerie-2018-11-08-HoTTEST.pdf and here is the talk: https://www.youtube.com/watch?v=JEUvWyd1mTk On Thursday, 8 November 2018 18:06:21 UTC, Ali Caglayan wrote: > > Hi, > > So after the HoTTEST seminar talk by Guillaume, it came to my attention > and many others that it could be possible to write tactics proving many of > these "holes" as they were put. Mortberg said some more on this. > > Let's have a discussion about this problem here. I think it would be > possible for the community to solve this problem. > > Guillaume's slides should be available later and the talk will be on > YouTube for those who missed it. At the time of writing this Email, which > is straight after the talk, they are not up. > > Thanks, > > Ali Caglayan > -- 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. For more options, visit https://groups.google.com/d/optout. ------=_Part_857_1066256179.1541749131790 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Here are the slides:

https://www.uwo.ca= /math/faculty/kapulkin/seminars/hottestfiles/Brunerie-2018-11-08-HoTTEST.pd= f

and here is the talk:

h= ttps://www.youtube.com/watch?v=3DJEUvWyd1mTk

On Thursday, 8 November= 2018 18:06:21 UTC, Ali Caglayan wrote:
Hi,

So after the HoTTEST semi= nar talk by Guillaume, it came to my attention and many others that it coul= d be possible to write tactics proving many of these "holes" as t= hey were put. Mortberg said some more on this.

Let= 's have a discussion about this problem here. I think it would be possi= ble for the community to solve this problem.

Guill= aume's slides should be available later and the talk will be on YouTube= for those who missed it. At the time of writing this Email, which is strai= ght after the talk, they are not up.

Thanks,

Ali Caglayan

--
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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_857_1066256179.1541749131790-- ------=_Part_856_1310116136.1541749131790--