# [Agda] Trust me regarding Dan Licata's trick

Martin Escardo m.escardo at cs.bham.ac.uk
Sat Jun 8 00:29:11 CEST 2013

Hank, it would be better if somebody else answered this, but here we go.

It is indeed the case that both == (propositional equality) and J
(induction on equality) look rather weird, and two decades were spent
exploring their weirdness by the cleverest people in our field.

Personally, I am not so interested (at the moment) in homotopy per se
(but I am interested in general topology and its relation to
computation, as you know). However, the homotopy interpretation of ==
and J made me understand why they are right, or at least why they are
the way they are.

Everything that is weird about == and J is natural about paths (==) and
path induction (J). If J were to be wrong, it is nevertheless very
surprising and exciting that it is the same thing as in a different,
venerable field, and probably worth exploring what this means and what
the two different fields have to contribute to each other, which is what
a number of people are doing.

This is, of course, with a pinch of salt, as the constructive content of
HoTT is open (and an active field of research). There are probably
complementary pinches of salt in the other field, but this is what makes
research exciting.

Imagine two plate tectonics colliding with each other: an earthquake is
what you would expect, and it is what we are getting.

Best,
Martin

On 07/06/13 22:33, Peter Hancock wrote:
> As a bystander, I was struck by this statement:
>
>> But, if we take ||-|| as primitive, we don't want to have a constant
>> for that equality: how would we compute with it? What would J do to
>> it?
>
> Are you sure that J, and the way it was introduced in type theory,
> is not in some way erroneous?  Why should we compute with J?  If ==
> is an inductive type, it is a very different inductive type, or family
> of types from all the others.
>
> Yes, we want to express an abstract equality somehow.  But perhaps not
> as a native type.  First ask what we need of such a notion, and then
> without charging in with too many preconceptions, (or in parallel
> with such experimentation) look carefully to see
> if there may be unexpected ways of getting (some of) what we want.
>
> I am thinking of Thierry Coquand's (non-computational) axiomatisation
> of equality from a year or two ago, not based on J, but incorporating
> univalence as an axiom. The computational
> meaning of equality might be obtained by modelling the axioms, somehow,
> in a type-theoretical meta-theory not involving this notion.
>
> Speculatively,
>
> Hank
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda