--- Day changed Thu Jul 27 2017
auguris there a new conventional way to do something kind of like a proof that the type checker tries to provide automatically?27/07 05:24
augurlike, implicit membership proofs?27/07 05:24
augurah! there is!27/07 05:26
apostolisHello27/07 16:26
apostolisI had a problem a few months ago where I wanted to prove that the function (\neg fun) is unique.27/07 16:30
apostolisI used irrelevance to avoid doing this.27/07 16:31
apostolisNow it seems that I cannot use irrelevance because the function is used.27/07 16:32
apostolisNow I am looking into proving the equality in Cubical TT, but I was wondering if there are easier solutions.27/07 16:33
apostolisThe fact that you are unable to prove uniqueness when you negate seems a very big problem to me.27/07 16:34
akrIs there a better way to write this? https://gist.github.com/osense/b2a24d5ac433a098a9b09e7d0968b974#file-print-agda-L3827/07 19:25
glguyakr: Probably not without dropping into the macro system27/07 21:58
akrah ok, nevermind then :)27/07 22:51

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!