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

[Ulf Norell]

I would make X and Y implicit. That's in line with the other cong functions
and as you say, they can often be inferred.

/ Ulf


On Wed, Feb 5, 2014 at 8:01 AM, Helmut Grohne <grohne at cs.uni-bonn.de> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140205/050993b6/attachment.html