[HoTT] Computer-generated proofs for the monoidal structure of the smash product

[HoTT] Computer-generated proofs for the monoidal structure of the smash product

[Ali Caglayan]

[-- 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 --]

[HoTT] Re: Computer-generated proofs for the monoidal structure of the smash product

[Ali Caglayan]

[-- 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 --]

[HoTT] Re: Computer-generated proofs for the monoidal structure of the smash product

[Anders Mörtberg]

[-- 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 --]