[Agda] Yet another questions about equality

[Thorsten Altenkirch]

Hi Hank,

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

Oh no - I was counting on you to stick up for the principles.

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

Sure, we know this already from Martin Hofmann's and Nicola Oury's work on the conservativity on Intensional Type Theory with Axioms over Extensional Type Theory. In this case one has to assume ext and uip (uniqueness of identity proofs). 
Univalence (Voevodsky's axiom) implies ext but is incompatibe with uip. In this case we haven't yet got an "extensional theory" to refer to. 

I do agree with your earlier remarks that we should be looking for a computational interpretation of ext and univalence. This should be a consequence of the fact that all constructions in Type Theory are compatible with those principles. E.g. we have no operation which distinuguishes extensionally equal functions and we have no operation which distinguishes weakly equivalent (and hence isomorphic) types.

The latter is easily broken in conventional set theory. I.e. neither union nor intersection are stable under isomorphism (And there were suggestions to introduce this sort of operations into Type Theory. The basic intuition in Type Theory is that you have to construct the set before you can construct any of its elements, while in Set Theory the elements are there first and the sets come later. Univalence is a consequence of this principle.

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

Yes, we should view this as a property of equality not its definition. I personally think it is sufficent if the computation rule for J holds propositionally (I know that Conor disagrees for pragmatic reasons).

Actually, our work on OTT exhibits the basic idea how to eliminate extensionality principles (I count univalence as an extensionality prinicple): we define equality by recursion over the structure of types and then recover the desired operations. In OTT we do this only for the non-dependent eliminator (subst) and then get away by using (definitional) uip. If we want to be able to capture univalence we have to work harder because we cannot use uip. And clearly the equality on the universe is just weak equivalence. So that's the plan but the details are tricky...

Cheers,
Thorsten