Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: "Anders Mörtberg" <andersmortberg@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Re: Computer-generated proofs for the monoidal structure of the smash product
Date: Fri, 9 Nov 2018 07:22:26 -0800 (PST)	[thread overview]
Message-ID: <48e8046d-006f-422f-93b2-c2b97c433ca4@googlegroups.com> (raw)
In-Reply-To: <defa749f-1c50-4b1c-bc10-5c9e90519888@googlegroups.com>


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

      reply	other threads:[~2018-11-09 15:22 UTC|newest]

Thread overview: 3+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-11-08 18:06 [HoTT] " Ali Caglayan
2018-11-09  7:38 ` [HoTT] " Ali Caglayan
2018-11-09 15:22   ` Anders Mörtberg [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=48e8046d-006f-422f-93b2-c2b97c433ca4@googlegroups.com \
    --to=andersmortberg@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).