[Agda] Vec _ n cong by n

[Sergei Meshveliani]

On Wed, 2013-06-19 at 20:16 +0200, Jesper Cockx wrote:
> I'm sorry, I didn't realize you were not familiar with inaccessible
> (dotted) patterns. There are other ways to define this function (for
> example by using the rewrite keyword), but dotted patterns are the
> most basic. Dotted patterns are a really useful technique when writing
> any program in agda with dependent types, and you shouldn't be afraid
> of them ;) You can use them whenever the types force a variable into a
> unique value (not very precise, but a good way to think about it). In
> this case, pattern matching on |xs|=n forces n to be equal to (length
> xs), hence the inaccessible pattern. 
> [..]

I thank you and Francesco for helpful remarks.

I knew the meaning of dotted patterns, but decided to avoid them --
while possible, and see further. I have forgotten of them, and now was
not able to use them in this concrete example.

Further, I have a feeling that something is strange in the Language.
Suppose that a type
                     Foo a

  depends on  a : C,  A : Setoid,  C = Carrier A, 
  the equivalence  p : a \~~ b   is proved,
  f : Foo a  is built,
  and we need to return  f : Foo b,
  and also somehow to express that  f : Foo a  can be replaced with  
  f : Foo b    if  a \~~ b.

Can this be expressed in Agda ?

Thanks,

------
Sergei



> [..]
>         
>         > On Wed, Jun 19, 2013 at 6:16 PM, Sergei Meshveliani
>         <mechvel at botik.ru>
>         > wrote:
>         >         Please, how to fix the following code?
>         >
>         >           f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec
>         ℕ n
>         >           f xs n |xs|=n =  v
>         >                            where
>         >                            v : Vec ℕ (length xs)
>         >                            v = fromList xs
>         >
>         >         The type of  v  does not match.
>         >
>         >         According to  |xs|=n,  length xs  can be replaced
>         with  n  in
>         >         Vec ℕ (length xs).
>         >         But probably,  cong  is not for  Vec  ...
>         >         So I wonder.
>         >
>         >         Thank you in advance for explanation,
>         >
>         >         ------
>         >         Sergei
>         >
>         >         _______________________________________________
>         >         Agda mailing list
>         >         Agda at lists.chalmers.se
>         >         https://lists.chalmers.se/mailman/listinfo/agda
>         >
>         >
>         
>         
>         
> 
>