[Agda] refl and pattern matching

[Martin Escardo]

As emphasized by Thorsten Alternikrch (maybe not in this list), it would 
be a nice project to prove that without-K works as intended, in 
particular regarding pattern matching against refl. Even the formulation 
of "as intended" may be tricky, let alone the proof. If I were to 
attempt this project myself, I would start from "lean" Martin-Loef type 
theory, without universes, and only with the basic types blessed by 
Martin-Loef in intensional type theory. Then at a second stage I would 
look for generalizations, including (various forms of) universes, and 
(various (useful and convincing) forms of) inductive/recursive 
definitions that came after Martin_Loef. Once pattern matching (without 
K) is properly understood in all proposed flavours of MLTT, I would 
attempt to argue about Agda. But life is short, and I have other 
projects in mind. So I wish such a project tempts somebody else with 
such inclinations.
Martin.
PS. I haven't answered your question. The reason is that I don't know 
the answer, which I explain above.


On 06/04/13 19:03, Andrés Sicard-Ramírez wrote:
> Hi,
>
> In http://thread.gmane.org/gmane.comp.lang.agda/4971/focus=4980 Martin
> Escardo wrote:
>
>     In fact, I would like to hear from the Agda developers and advisors how
>     close or far Agda is from the MLTT family of type theories.
>
>     ...
>
>     (1) Pattern matching.
>
>           Is fine provided refl is not a pattern (except for the definition
>           of J).  Good to have without-K, but not so good that there isn't a
>           theory of pattern matching without K, or any assurance that
>           without-K actually works. This is particularly relevant for the
>           HoTT enthusiasts using Agda.
>
>
> Assuming that the option --without-K works, why I cannot use refl in
> pattern matching (except for the definition of J) ?
>
> Thanks,
>
> --
> Andrés
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe