[Agda] Yet another questions about equality

[Peter Hancock]

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

In the interest of restoring balance to the universe, I've changed my mind.
Seriously, this presentation by T. Coquand:
http://www.cse.chalmers.se/~coquand/bologna.pdf
seems to suggest (see the end) that it may be possible to treat
the identity types purely axiomatically, with no computation rules.
(Nils Danielsson has had a hand in this too.)

When trying to follow arguments that make heavy use of abstract equality,
for example, many constructions in category theory, I find I can follow
them only as a formal game, that starts: "let us pretend we know what
propositional equality means. Then ...".  So I cross my fingers, pray silently that
no real harm will come of it, and try to play the game.

Maybe propositional equality is an *ideal* notion, in something like the sense of
Hilbert's programme?  What we want to know is some kind of conservative
extension result: that so far as *real* (inductively defined) types go,
there are no new terms, up to definitional equality.  Or something like that.

There is certainly something "fatuous" (I can't think of a better word)
about the computation rule for J -- in the same way as there is something
fatuous about the elimination rule for the singleton rule for N_1 (the
standard singleton set).

Peter Hancock