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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 33a7dff2 for ; Thu, 8 Nov 2018 18:06:24 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id j18sf13055467oth.11 for ; Thu, 08 Nov 2018 10:06:23 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=vDFDa3CJTdJdVEmTmDeMdbEm2OdHmQ2Kfswp231FbgM=; b=I6uZ6nROzBG9kP4H53Wj9P9yrXpxwGa2M2dmt29UorWJsVfiP2Wr4NVN7l1QLg9ImB uy/LhRBWu7NGk68lBJ7HRmHKKrsktG4mkz8O/uLKOup9QjIRrQHYMraTyBwL9xgaSRax xX2wbl55WAzWsg2oJPw1ayFrJ3FQIPEK7csGwQEqTFvWNJ26mbd6tjXE4r5cVmG3DMqy oms+CzV719jqqySAgGKKAaXU5wzC91bdZ3lPLoXUKI+4bTc6Kp3qF0hCdG76ts91Ok/d SLRHijSwJs4LE6Ft+Yfnd13PcyEzo4b7IFyThLfKyvjRfrZeEgl0U+K4rZmgKm8SMQly vTfQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=vDFDa3CJTdJdVEmTmDeMdbEm2OdHmQ2Kfswp231FbgM=; b=US6+7fTCirXLXFFw38pxXstaLaZZqVG11CSw7lMMeAZdVd9rOC+MXVBorD8Pbzmb8Q qFn/URoC2rSWKXi0l3Guml6xwmTpx4WdHiM52nMMm2scLzqePcOKuXNvSKs9YX9u+2Tu XBF/VIftR6gulI4X7e54kfC7ksBNvzMwlHFe3/bcAwYql6wl9Tusn8a56PQi9toAaXUq X+34wmMxX2byTdPGCRv9UHeutO6YL/8XBlcvHR6Tv4l0tUL8ghq9rRaRw29v41Kp0qgY 0bQ86z7WJUZDKUEV2z8wD5vw6Rm/nCN0Tam+sHxiv59LEprvJv1qD+0iCBg3oxT4eI4i IzQA== 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: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=vDFDa3CJTdJdVEmTmDeMdbEm2OdHmQ2Kfswp231FbgM=; b=J3TfP8/+S+gQLK/BRQ8eMf2nPIDjBWTH1ff8osKKY8sRoPZgdi7kjtr+0C49oG1Vku ngbxc3mRbK8uo2Ii/GJfZ72VCoUmKqHI3OWoTSHsNTSNWnDu8XtSP19DmzciP2laAOx4 o0/PeUZlS4+TmVHnNaHA7HnGqtMN5ggfNMIJqqOKJ+zqfwbEyRsOyAASs/3mLcDhP7cR SQXeyqJCBm4wAFN/gm1PnKX8lJbRtEekmU1jji7/eoIQwNLMKuZJ1mkrTKoc53xRvHj2 wxMuwIVapHzRkJnp8muLg6uzoL71I/yxMBl/AERA8sPn3vQZcVGECu5ibUIQVXVHlNAM pGQQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLafGTG8g1IaD2UtcaRgwxYmmfuEAysxkPPIz8KhjWEl7Wpsj3K WKz6H+tmf2M50lXUNCGz0ho= X-Google-Smtp-Source: AJdET5cWvMF/UrMr/fTUC0NdXXVrHs/y0kH75wQbLtsb46c6qPljpAHpN1k46KkjBLQDxZjD7IX0Bg== X-Received: by 2002:a9d:5403:: with SMTP id j3mr92972oth.2.1541700382748; Thu, 08 Nov 2018 10:06:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:c154:: with SMTP id r81-v6ls1205053oif.12.gmail; Thu, 08 Nov 2018 10:06:22 -0800 (PST) X-Received: by 2002:aca:ad0a:: with SMTP id w10-v6mr51400oie.2.1541700382094; Thu, 08 Nov 2018 10:06:22 -0800 (PST) Date: Thu, 8 Nov 2018 10:06:21 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <8a0d0d80-2ee6-471d-b5e6-f9aefdc7b7af@googlegroups.com> Subject: [HoTT] Computer-generated proofs for the monoidal structure of the smash product MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_575_636828397.1541700381492" 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_575_636828397.1541700381492 Content-Type: multipart/alternative; boundary="----=_Part_576_179547167.1541700381492" ------=_Part_576_179547167.1541700381492 Content-Type: text/plain; charset="UTF-8" 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_576_179547167.1541700381492 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi,

So after the HoTTEST seminar talk b= y Guillaume, it came to my attention and many others that it could be possi= ble to write tactics proving many of these "holes" as they were p= ut. Mortberg said some more on this.

Let's hav= e a discussion about this problem here. I think it would be possible for th= e 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,
<= br>
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_576_179547167.1541700381492-- ------=_Part_575_636828397.1541700381492--