<div dir="ltr">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.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Wed, Feb 5, 2014 at 8:01 AM, Helmut Grohne <span dir="ltr"><<a href="mailto:grohne@cs.uni-bonn.de" target="_blank">grohne@cs.uni-bonn.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi,<br>
<br>
While using heterogeneous equality from the standard library I found a<br>
need unaddressed. I was unable to cong a Data.Vec.map f to a<br>
heterogeneous equality using the provided toolbox. When looking at the<br>
most relevant tool<br>
<br>
cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}<br>
(f : (x : A) → B x) → x ≅ y → f x ≅ f y<br>
cong f refl = refl<br>
<br>
one can see why usage with Data.Vec failed. The function to be passed,<br>
has to have a single domain type, but the map function has an indexed<br>
domain.<br>
<br>
Thus I am proposing the addition of an indexed version of cong to the<br>
standard library. Thus far I have been using the following version:<br>
<br>
i-cong : ∀ {l m n} {I : Set l} (X : I → Set m) (Y : I → Set n)<br>
(f : {i : I} → X i → Y i) {i j : I} → i ≡ j →<br>
{x : X i} {y : X j} → x ≅ y → f x ≅ f y<br>
i-cong X Y f P.refl refl = refl<br>
<br>
It is indexed, but non-dependendent (unlike the original cong). So this<br>
yields the question of whether this is the "right" cong to add, or<br>
whether it should go even further and support both indexing and<br>
dependence.<br>
<br>
When using i-cong it is not clear to me whether Y really should remain<br>
and explicit parameter, because it can be inferred in many cases.<br>
<br>
Helmut<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>