[Agda] RFC: R.B.HeterogeneousEquality + i-cong

[Helmut Grohne]

Hi,

While using heterogeneous equality from the standard library I found a
need unaddressed. I was unable to cong a Data.Vec.map f to a
heterogeneous equality using the provided toolbox. When looking at the
most relevant tool

cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}
       (f : (x : A) → B x) → x ≅ y → f x ≅ f y
cong f refl = refl

one can see why usage with Data.Vec failed. The function to be passed,
has to have a single domain type, but the map function has an indexed
domain.

Thus I am proposing the addition of an indexed version of cong to the
standard library. Thus far I have been using the following version:

i-cong : ∀ {l m n} {I : Set l} (X : I → Set m) (Y : I → Set n)
         (f : {i : I} → X i → Y i) {i j : I} → i ≡ j →
         {x : X i} {y : X j} → x ≅ y → f x ≅ f y
i-cong X Y f P.refl refl = refl

It is indexed, but non-dependendent (unlike the original cong). So this
yields the question of whether this is the "right" cong to add, or
whether it should go even further and support both indexing and
dependence.

When using i-cong it is not clear to me whether Y really should remain
and explicit parameter, because it can be inferred in many cases.

Helmut