<div dir="ltr"><span style="font-size:12.8px">Thank you, Nils!</span><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">I was not aware of "abstract" as a language feature. I will keep it in mind and I have made all my equivalence proofs abstract. It still takes a significant amount of time to type check the triangle identity but it eventually type checks now.</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">I tried to add the last postulate I need, but even though I now have marked all of the proofs as abstract the compilation time is again at 30+ minutes with no end in sight:</div><div style="font-size:12.8px"><br></div><div><span style="font-size:12.8px"><a href="https://github.com/jbracker/polymonad-proofs/blob/ec730f224eedb478cfdfb277c7eea2503dae5771/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates/PentagonId.agda">https://github.com/jbracker/polymonad-proofs/blob/ec730f224eedb478cfdfb277c7eea2503dae5771/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates/PentagonId.agda</a></span><br></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px"><br></span></div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-26 15:33 GMT+01:00 Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2017-06-23 12:42, Jan Bracker wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
What really baffles me is that these are postulates. I do not<br>
understand why the compiler should ever take any significant amount of<br>
time to check them.<br>
</blockquote>
<br></span>
I think Agda has trouble checking that the last equality type that you<br>
give is well-formed.<br>
<br>
I managed to get the code to type-check by adding a large number of<br>
"abstract" annotations to your code (and postulating a single lemma that<br>
failed to type-check), see the attached patch. I suggest that you try to<br>
make all of your "proofs" abstract.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>