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

[Ulf Norell]

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:

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 P.≡ j →
         {x : X i} {y : X j} → x ≅ y → f x ≅ f y
i-cong f P.refl refl = refl

module _
  (A B : Set)
  (n m : ℕ)
  (xs : Vec A n)
  (ys : Vec A m)
  (n=m : n P.≡ m)
  (xs=ys : xs ≅ ys)
  (f : A → B) where

  thm : map f xs ≅ map f ys
  thm = i-cong (map f) n=m xs=ys

/ Ulf


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

> On Wed, Feb 05, 2014 at 08:24:23AM +0100, Ulf Norell wrote:
> > 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.
>
> I'm sorry, but that doesn't work. At the very least X must be explicit
> (like P is explicit for subst). The question was only about Y.
>
> 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/64b33974/attachment.html