[Agda] Re: How can I prove associativity of vectors?

[Andreas Abel]

Hello Helmut,

I read the thread you pointed to below, and found that the discussion 
was stuck on whether to make X and Y implicit or not.  Ulf gave the 
following example:

open import Data.Nat
open import Data.Vec

import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality

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

You say this leaves some unsolved metas in Agda 2.3.2.2.  At least in 
2.4.3 (current development version) all metas are solved.

This would mean that the above definition of i-cong can be taken?!

Cheers,
Andreas

On 17.12.2014 18:05, Helmut Grohne wrote:
> On Wed, Dec 17, 2014 at 11:44:28AM +0200, Andreas Abel wrote:
>> The hcong' you suggest would be a nice addition to the standard
>> library.  Feel free to create a pull request to
>>
>>    https://github.com/agda/agda-stdlib
>
> This was suggested earlier, but Ulf Norell was not happy with it. The
> corresponding thread starts at:
>
> https://lists.chalmers.se/pipermail/agda/2014/006464.html
>
> If there is consensus now that we do want it, I can submit a git branch
> for including it (next year).
>
> Helmut
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/