[-- Attachment #1.1: Type: text/plain, Size: 855 bytes --] 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. [-- Attachment #1.2: Type: text/html, Size: 1182 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1135 bytes --] 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. [-- Attachment #1.2: Type: text/html, Size: 1659 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3111 bytes --] 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. [-- Attachment #1.2: Type: text/html, Size: 4949 bytes --]