[Agda] Yet another questions about equality

[Thorsten Altenkirch]

On 16 Feb 2011, at 11:48, Andreas Abel wrote:

> Hi Thorsten,
> 
> On 2/16/11 1:17 PM, Thorsten Altenkirch wrote:
>> Btw, I completely agree with Peter Hancock that we should use/look
>> for a computational sound interpretation of ext (such as OTT).
>> However, OTT and my earlier LICS paper rely on proof irrelevance
>> which is incompatible with the recent developments related to
>> univalent foundations (which is basically a strengthening of ext by
>> considering an extensional equality of sets called weak
>> equivalence).
> 
> Proofs of small equalities (equalities between terms) can still be irrelevant, as I understood it.  It is sufficient to have one proof of 0=0, since there are no isomorphisms between 0 and 0. ;-)

Yes, all small sets (i.e. A : Set_0) have H-level 2, i.e. UIP holds. However, this is rather a coincidence which may fail to hold in the future - in particular if one introduces proof-relevant quotients.

> Can't OTT work with that restricted proof irrelevance?

If you restrict yourself to Set_0. But this seems quite unnatural.

Cheers,
Thorsten

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110218/04fb1c38/attachment.html