[Agda] Yet another questions about equality

[Peter Hancock]

...
>> 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.)
>
> If you're talking about him mentioning the connection with OTT, it was my
> impression that he was suggesting that the univalent foundations extend OTT
> such that there _is_ a proper computational interpretation of equality.

I'm referring to the 6 axioms developed in the talk (slide 48), and the
last slide (58). To quote:

   These works rely on special computation rules for equality
   Nils Anders Danielsson has proved formally that we don’t need new computation rules
   (axioms are enough).

Well, I guess I don't quite know what this means, but I'm encouraged to find out
by going through what can be done with Thierry's axioms.

> Specifically, equality of sets is interpreted as isomorphism, instead of being
> true along the diagonal, and false otherwise.

If I understand univalent foundations (I don't -- but I have listened twice to
Nicola Gambino explain V's proof that his axiom implies function
extensionality), it is an axiom about *small* sets (for which it makes sense
to say propositionally that they are identical).  I personally would prefer not
to entangle this too much with the idea that all sets are contained in a universe.
I've been told that V's work in parts depends quite heavily on a specific
conception of universes.

>
>> 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).
>
> I'm not exactly sure what your meaning is here.

Well, I'm not exactly sure myself.  The development of type theory has been
very much bound up with getting a clear view of equality: first definitional
equality, and then propositional equality. I'm not sure the situation isyet
satisfactory with respect to either of these.  My opinion is that, till recently,
development has been stalled for at least a decade, and some extremely radical shift or shifts in perspective
are needed.  Whatever one thinks of univalent foundations, whatever they are,
at least there's reason to be hopeful it may be at last a shift happening.  I have
no idea what what will emerge.

As for the "inductive" propositional equality ("the least reflexive relation"),
that notion was reasonably clear when logicians were studying inductive definitions
over the natural numbers, or in a first order system based on predicate logic
(like in Martin-Lof's very influential paper on inductive definitions, from
1972 or something).  The problem is, there is no non-trivial definitional
equality involved in these systems, at least explicitly.  Relatively speaking,
its reasonably clear what it should mean with respect to expressions for finite
(syntactic) objects, or natural numbers.  For higher order objects, I think
it is, or should be, much more controversial.

> However, it's kind of
> interesting to note that type theorists would usually suggest that the J
> induction rule, and its computation, works because there is one canonical way
> of proving equality: refl. So when we write:
>
>    J : P x refl ->  P y eq, A : Type, x : A, P : (y : A) ->  x = y ->  Type
>
> it must work because y must be x, and eq must be refl. Univalent foundations
> suggest that this needn't actually be the case when x and y are themselves
> sets. But we still have J. What does this mean? It means that predicates on
> sets P themselves hold only up to isomorphism on sets. So we are not justified
> because y must be x, and the proof must be refl, but because x and y are
> isomorphic, and there is a way to transport a proof of P x refl along the
> isomorphism to a proof of P y eq (and similar for higher-dimensional types).

There are all sorts of shades of meaning involved in saying something
like: x must *be* y, or the *same* as y -- or, for that matter, "x"
*means* the same as "y", or has the same *reference* as "y", or lie on the
*diagonal*, or a hundred other circumlocutions.  I really despair of
arriving at a clear conception of equality by turning up my knob
of linguistic sensitivity, like a microscope, till suddenly, it equality,
(or any notion built on top of it, like isomorphism) locks into focus.

For what it is worth, probably very little, I sometimes find myself
wondering whether equality means anything at all.  This is a bit
uncomfortable, as my dentist sometimes puts says.  For comfort, I
sometimes think of what other people have said, like Wittgenstein:  
‘Roughly speaking, to say of two things that they are identical is nonsense,
and to say of one thing that it is identical with itself is to say nothing at all.’

I hope these is something above that isn't entirely ranting.

Peter Hancock