<div dir="ltr">It's not the same situation as in subst. You can infer both X and Y from the type of f in many cases. Here's your motivating example:<div><br></div><div><div>i-cong : ∀ {l m n} {I : Set l} {X : I → Set m} {Y : I → Set n}</div>
<div> (f : {i : I} → X i → Y i) {i j : I} → i P.≡ j →</div><div> {x : X i} {y : X j} → x ≅ y → f x ≅ f y</div><div>i-cong f P.refl refl = refl</div><div><br></div><div>module _</div><div> (A B : Set)</div>
<div> (n m : ℕ)</div><div> (xs : Vec A n)</div><div> (ys : Vec A m)</div><div> (n=m : n P.≡ m)</div><div> (xs=ys : xs ≅ ys)</div><div> (f : A → B) where</div><div><br></div><div> thm : map f xs ≅ map f ys</div><div>
thm = i-cong (map f) n=m xs=ys</div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Feb 5, 2014 at 8:59 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"><div class="im">On Wed, Feb 05, 2014 at 08:24:23AM +0100, Ulf Norell wrote:<br>
> I would make X and Y implicit. That's in line with the other cong functions<br>
> and as you say, they can often be inferred.<br>
<br>
</div>I'm sorry, but that doesn't work. At the very least X must be explicit<br>
(like P is explicit for subst). The question was only about Y.<br>
<div class="HOEnZb"><div class="h5"><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>
</div></div></blockquote></div><br></div>