Hi,<br><br>In <a href="http://thread.gmane.org/gmane.comp.lang.agda/4971/focus=4980">http://thread.gmane.org/gmane.comp.lang.agda/4971/focus=4980</a> Martin Escardo wrote:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">

In fact, I would like to hear from the Agda developers and advisors how <br>close or far Agda is from the MLTT family of type theories.<br><br>...<br><br>(1) Pattern matching.<br><br>     Is fine provided refl is not a pattern (except for the definition<br>

     of J).  Good to have without-K, but not so good that there isn&#39;t a<br>     theory of pattern matching without K, or any assurance that<br>     without-K actually works. This is particularly relevant for the<br>     HoTT enthusiasts using Agda.<br>

</blockquote><br>Assuming that the option --without-K works, why I cannot use refl in pattern matching (except for the definition of J) ?<br><br>Thanks,<br><br>--<br>Andrés