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