Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Computer-generated proofs for the monoidal structure of the smash product
@ 2018-11-08 18:06 Ali Caglayan
  2018-11-09  7:38 ` [HoTT] " Ali Caglayan
  0 siblings, 1 reply; 3+ messages in thread
From: Ali Caglayan @ 2018-11-08 18:06 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 855 bytes --]


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.


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

^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2018-11-09 15:22 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-11-08 18:06 [HoTT] Computer-generated proofs for the monoidal structure of the smash product Ali Caglayan
2018-11-09  7:38 ` [HoTT] " Ali Caglayan
2018-11-09 15:22   ` Anders Mörtberg

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).