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-oi1-x240.google.com (mail-oi1-x240.google.com [IPv6:2607:f8b0:4864:20::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 330f6cd0 for ; Fri, 9 Nov 2018 15:22:28 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id a188-v6sf1140386oih.0 for ; Fri, 09 Nov 2018 07:22:28 -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=2s9TioCV+jEFdPmoXaGfQAno8qUGuEKS+setzunqyNw=; b=YIsnTjQhT74Gs1Boq9DCvhkgJy8xab8IjGDUIbh1Bj0TVdf2IKNeUpXq0SrBd0mb8I HbSw4rGF1HpbI0lx4l9IwlzPi7cnEy7IoYel02uwn63wSFN+7zuC9P4BLmPjjxYRe4D2 KAxp5RqpLRbbY+K/+dl0A/CBJNzX5WwM3phqxgsrDTi9qWmlfZDJzN9VK3nouk6WNLd/ N8uDNkx8LqShx702I5OOxUdDn9+2PDehlpLti3bCtGTcIy8p0a5qixSuSd7kFx9Lwq86 4d6vqLhaB/wcIkeyqipdtwrUQY8VKSE8id5ABVPladJSW+qr9lKb/TTXilr4nCNBbsFl PmRA== 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=2s9TioCV+jEFdPmoXaGfQAno8qUGuEKS+setzunqyNw=; b=VjUvpWeQJzPLXmnwwHbFou1Yy/GusncWM7PtCh8bBpepZAYfSBeCYil/fmdJNoiAPv 1iUzybgGj42OyBut5IA9WDdcrz+ghNxSCza9qYZ+QJtpwYiLkVSCQk4aJ/bDqZBI2mKo ppQKJE6hIaFG8ik8Zc8zx0PczA9ev8wRtrUmrSIFRItM3jdCfNMAky7bw0LjJ/QunYWc AveBOL8Vkpzy1Be2sSHpIo3Ex3CZ04ljaCfsuX/i+RawMx8yoHWsD3/WQ1tY12VupJ0J RTgqz7W0YRxJatdSQL8CSJLCoTGah+LOsc0Um9jsNQISaJXipAYWBRi0vg//c0d/qc53 u2wQ== 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=2s9TioCV+jEFdPmoXaGfQAno8qUGuEKS+setzunqyNw=; b=WL0S5VJobnZt3zU24V4tFYzVqK5GNtp9jID+Gy8WJ8ru6sfvvqiQGsBkcVM5Sei+dN xhNKsPjwJu1qR4+nRH6bNgy9M+BnpxF2fP054Axg8IqjlfqWJYBAaJp0NrA1JAPDZMoy G7rPmvyDiyUqrHY4GVJqAcBto/Tb8k8esD5ZtdVl+fEmXItRLCZDjUbFkqokZQ/VmqR0 PqthX2sE5pV6OSRWYfmeMkjfkwSRg4iXqU6THNKrdDih4fIgvUtjM/Ti8BX3UCajc5ug 2lx1as/wi46UoY03rFnFXsTtcCLSsQBj+17RcXR3qadJqfIc3QDa3VewQ9eVIvrMu4Sd ldHA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKxyvqvhlL6dzFGiNmawWj0A6/P+mP8tw63aBLPqPHQDN8OzUho MNJTpdPY92RLaKTk0XqTvNg= X-Google-Smtp-Source: AJdET5fsf2DSK5+6gxL7BHQFz/+TJWAAb3QA1YkxYKT4iiyqzJSW86QLgdJklRm26dJalMTPDbzUKw== X-Received: by 2002:a9d:5403:: with SMTP id j3mr153788oth.2.1541776947741; Fri, 09 Nov 2018 07:22:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3444:: with SMTP id b65-v6ls891332oia.1.gmail; Fri, 09 Nov 2018 07:22:27 -0800 (PST) X-Received: by 2002:aca:37c1:: with SMTP id e184-v6mr99789oia.5.1541776947188; Fri, 09 Nov 2018 07:22:27 -0800 (PST) Date: Fri, 9 Nov 2018 07:22:26 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <48e8046d-006f-422f-93b2-c2b97c433ca4@googlegroups.com> In-Reply-To: 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_993_883760918.1541776946683" X-Original-Sender: andersmortberg@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_993_883760918.1541776946683 Content-Type: multipart/alternative; boundary="----=_Part_994_627066685.1541776946683" ------=_Part_994_627066685.1541776946683 Content-Type: text/plain; charset="UTF-8" Just some clarification, Jon Sterling said things about using tactics from my account after the talk, not me. :-) I personally don't think it would be very interesting to try to redo Guillaume's proof in a system like Coq/Lean using tactics. What I find interesting is to design new type theories with better/proper support for HITs in which these proofs should be more convenient to do because of more definitional equalities. Two such new systems are Cubical Agda and redtt. I defined the smash product and proved that commutatitivity is an involution in Cubical Agda earlier this week and it was completely trivial: https://github.com/agda/cubical/blob/master/Cubical/HITs/SmashProduct.agda I started doing the associativity map but stopped as it was getting too complicated, but Evan Cavallo managed to finish this in redtt: https://github.com/RedPRL/redtt/blob/smash/library/cool/smash.red The definition is very long and I absolutely don't think that it will be easy to prove anything about it in Cubical Agda or redtt, but hopefully one could do something similar to what Guillaume did in regular Agda or using tactics in redtt to generate the more complicated proofs. I'm optimistic that the proof terms will be substantially smaller and hence require less memory and time to typecheck. A well-known "issue" with both Cubical Agda and redtt is that J does not compute on refl for Path-types, however I wonder how much of an issue this really is in practice. In "book HoTT" both the eliminators for HITs doesn't compute on higher constructors and ap doesn't compute on identity or composition, which seems like more serious "issues" to me, especially for the proofs that Guillaume was showing yesterday. Furthermore, if one really needs J to compute on refl then one can just use the cubical Id types in Cubical Agda. Best, Anders On Friday, November 9, 2018 at 2:38:51 AM UTC-5, Ali Caglayan wrote: > > 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_994_627066685.1541776946683 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Just some clarification, Jon Sterling said things abo= ut using tactics from my account after the talk, not me. :-)

=
I personally don't think it would be very interesting to try= to redo Guillaume's proof in a system like Coq/Lean using tactics. Wha= t I find interesting is to design new type theories with better/proper supp= ort for HITs in which these proofs should be more convenient to do because = of more definitional equalities. Two such new systems are Cubical Agda and = redtt. I defined the smash product and proved that commutatitivity is an in= volution in Cubical Agda earlier this week and it was completely trivial:

https://github.com/agda/cubical/blob/master/Cubical= /HITs/SmashProduct.agda

I started doing the associ= ativity map but stopped as it was getting too complicated, but Evan Cavallo= managed to finish this in redtt:

https://github.c= om/RedPRL/redtt/blob/smash/library/cool/smash.red

= The definition is very long and I absolutely don't think that it will b= e easy to prove anything about it in Cubical Agda or redtt, but hopefully o= ne could do something similar to what Guillaume did in regular Agda or usin= g tactics in redtt to generate the more complicated proofs. I'm optimis= tic that the proof terms will be substantially smaller and hence require le= ss memory and time to typecheck.

A well-known= "issue" with both Cubical Agda and redtt is that J does not comp= ute on refl for Path-types, however I wonder how much of an issue this real= ly is in practice. In "book HoTT" both the eliminators for HITs d= oesn't compute on higher constructors and ap doesn't compute on ide= ntity or composition, which seems like more serious "issues" to m= e, especially for the proofs that Guillaume was showing yesterday. Furtherm= ore, if one really needs J to compute on refl then one can just use the cub= ical Id types in Cubical Agda.


Best= ,
Anders


On Friday, November 9, 2018 at 2= :38:51 AM UTC-5, Ali Caglayan wrote:


<= /div>

--
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_994_627066685.1541776946683-- ------=_Part_993_883760918.1541776946683--