[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

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