[Agda] Re: Builtins

[N. Raghavendra]

At 2015-04-25T21:47:23Z, Kirill Elagin wrote:

> Simply put, it is the ability to pattern-match on `refl` that gives
> you the K axiom and the uniqueness of identity (which follows from K).

Thanks again for your explanation!

> The funny thing is that, as far as I know, it is not proven that
> there is no other way to derive K, using, maybe, some other weird
> trick with pattern matching. So the `--without-K` is not guaranteed
> to save you from K, but it is believed to do so.

Yes, there are messages now and then about this on the HoTT mailing
list.  I am following the method described in
http://ncatlab.org/homotopytypetheory/show/Agda, and am trusting that
--without-K is indeed safe.

Cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/