[Agda] Yet another questions about equality

[Andreas Abel]

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. ;-)

Can't OTT work with that restricted proof irrelevance?

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/