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

[Sergei Meshveliani]

On Thu, 2014-12-18 at 14:41 +0400, Sergei Meshveliani wrote:
> On Wed, 2014-12-17 at 20:38 +0100, Andrea Vezzosi wrote:
> > The following seems to work:
> > 
> > open import Data.Nat
> > open import Data.Vec
> > open import Relation.Binary.PropositionalEquality
> > 
> > postulate
> >   x y : ℕ
> >   x=y : x ≡ y
> > 
> > to : Vec ℕ x → Vec ℕ y
> > to = subst (Vec ℕ) x=y
> > 
> > from = subst (Vec ℕ) (sym x=y)
> > 
> > [..]
> 
> 
> Thank you for explanation. 
> `subst' occurs more generic than I used to think of it.
> 
> I rewrite your code into this:
> 
>  vecCong-iso :  ∀ {A : Set} → ∀ {m n} → m ≡ n → Vec A m → Vec A n
>  vecCong-iso {A} =  PE.subst (Vec A)
> 
> I think, this expresses that  (Vec A)  preserves _≡_ respectively to the
> domain (type) identity.
> [..]

I need to add:  "modulo this isomorphism".

------
Sergei