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

[Dan Licata]

It's also related to "uniqueness of identity proofs" (UIP). If I recall correctly, the Hofmann and Streicher paper on The Groupoid Interpretation of Type Theory explains the various forms of this principle. 

-Dan

On May 29, 2013, at 3:16 PM, Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda