[Agda] Re: Yet another way Agda --without-K is incompatible with univalence

[Matteo Acerbi]

As the parameterised version was not accepted, I incorrectly thought
the problem was related to using "postulate" there. I should have
checked this was not the case before sending a useless comment, my
sincere apologies. :-)

Thank you very much for the precise explanation.

When I have more time I will try to understand the details of Agda's
pattern matching and the various attempts at "--without-K".

Cheers,
Matteo