[Agda] ANNOUNCE: Agda 2.2.10

[Dan Doel]

On Tuesday 22 February 2011 1:30:57 PM you wrote:
> >> > data Eq (A : Set) (a : A) : .A ->  Set where
> >> > 
> >> >    refl : Eq A a a
> > 
> > This definition should simply not be allowed, I'd say. If we think about:
> > 
> >  Eq A a : .A -> Set
> > 
> > then this means that the second A should be irrelevant for the purpose of
> > determining what _set_ is returned. Which implies that Eq A a b and Eq A
> > a c should be in some sense the same set even if b and c are different.
> > But this is clearly not what Eq is trying to accomplish.
> 
> Maybe, this is in fact what Eq is trying to accomplish (in some sense). :)

Is it? Here's the situation I can come up with in which it could actually be 
used:

  foo : (A : Set) (x : A) .(y : A) -> Eq A x y -> ...
  foo A x .x refl = ...

However, Agda doesn't yet have dependent irrelevance, so this type can't 
actually be written. And of course, 'refl' proves Eq A x y for all y, 
regardless of type, so it's not the usual equality. I guess it has 
applications if you want to refine an irrelevant parameter (which I can 
conceive of being useful, at least). Sorry if this was your intent, and I 
missed it. I was thinking this was expected to be the normal equality.

I expect having a match on refl refine a relevant parameter is a no-no, 
though. There's no reason to expect Eq A x y's inhabitation to imply x = y.

In the meantime, the following works, and may get part of the way there:

  data Squash (A : Set) : Set where
    squash : .A -> Squash A

  data Eq (A : Set) (x : A) : Squash A -> Set where
    refl : Eq A x (squash x)

  bar : (A : set) (x : A) (y : Squash A) -> Eq A x y -> ...
  bar A x .(squash x) refl = ...

Since Agda doesn't have dependent irrelevance, you can in theory replace all 
'.A -> ...' with 'Squash A -> ...' I think, and use the above. Not that that's 
pleasant.

-- Dan