[Agda] Trust me regarding Dan Licata's trick

[Peter Hancock]

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