* [HoTT] Re: Computer-generated proofs for the monoidal structure of the smash product
2018-11-09 7:38 ` [HoTT] " Ali Caglayan
@ 2018-11-09 15:22 ` Anders Mörtberg
0 siblings, 0 replies; 3+ messages in thread
From: Anders Mörtberg @ 2018-11-09 15:22 UTC (permalink / raw)
To: Homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 3+ messages in thread