[Agda] A correctness proof for pattern matching without K

[Martin Escardo]

On 10/03/14 14:28, Jesper Cockx wrote:
> Some people might be interested that I finished the correctness proof
> for pattern matching without K. 

I have now tested it in a large collection of Agda files, and it works
wonderfully. Thanks!

(Wouldn't it be better if the patch simply made without-K work in your
way, rather than require to change all files from without-K to
new-without-K?)

Even one file that used to be rejected by without-K is now accepted by
new-without-K. http://www.cs.bham.ac.uk/~mhe/agda/SumDisjoint.html

But I have a question regarding that file:

It proves the following:
> [...]
> Let f be a function defined by dependent pattern matching (i.e. it has a
> valid case tree and is structurally recursive), where all case splits
> follow the restrictions above. Then we can translate f to a definition
> using only eliminators (/without/ using the K axiom).

I wonder what your automatic translation of my function in the above
file to eliminators is. The reason I am asking is that what I prove
above using pattern matching requires the use of a universe in MLTT.
Does your automatic translation generate such a use of the universe?

M.