[Agda] heterogeneous equality

[Dan Licata]

On Mar03, Conor McBride wrote:
> Back when I was mucking about with this type,
> my answer was "homogeneously"! That's to say,
> rather than interpreting heterogeneous equality
> as "the types are equal and the terms are equal",
> it's "if the types are equal, the terms are equal".

Ah, I had the conjunctive, rather than conditional, interpretation in
mind. Thanks for the explanation!

Last night, the workaround I came up with was to take in a proof p of
index equality and to prove that e is (homogeneously) equal to 
(subst e' p).  E.g.

waha : {X : Set}{m n : Nat}
       {xs : Vec X m}{ys : Vec X n}{x : X} ->
       (p : Id m n) (sp : Id (suc m) (suc n))
     -> Id (subst (\i -> Vec X i) xs p) ys
     -> Id (subst (\i -> Vec X i) (cons x xs) sp) (cons x ys) 

The heterogeneous version then seems like a simple twist that saves you
from manually commuting-converting the subst in and out of contexts---as
you said, I can work with a telescope, rather than coercing everything
to the same type at each step.


The conjunctive interpretation, which post-darcs-pull Agda moves
towards, feels a little impredicative: it makes me nervous to have a
set of equality of sets, since this set "talks" about itself.  Are there
dangers lurking under this tarpeian rock?  


-Dan