[Agda] refl and pattern matching
m.escardo at cs.bham.ac.uk
Sat Apr 6 20:57:17 CEST 2013
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
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:
> 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) ?
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda