<div dir="ltr">It&#39;s not the same situation as in subst. You can infer both X and Y from the type of f in many cases. Here&#39;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">&lt;<a href="mailto:grohne@cs.uni-bonn.de" target="_blank">grohne@cs.uni-bonn.de</a>&gt;</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>
&gt; I would make X and Y implicit. That&#39;s in line with the other cong functions<br>
&gt; and as you say, they can often be inferred.<br>
<br>
</div>I&#39;m sorry, but that doesn&#39;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>