[Agda] --without-K option too restrictive?

[Andrés Sicard-Ramírez]

On 29 May 2013 14:08, Jason Gross <jasongross9 at gmail.com> wrote:
> The K-rule is Streicher's axiom K.  A brief google search for "axiom K"
> gives me http://ncatlab.org/nlab/show/axiom+K and
> http://adam.chlipala.net/cpdt/html/Equality.html.

There is also a nice presentation in Ulf Norell's PhD thesis, section 1.5.2.

-- 
Andrés