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

[flicky frans]

Moreover, it's easy to define `icong' in terms of `cong₂'

    icong : ∀ {α β γ} {I : Set α} {i j : I}
          -> (A : I -> Set β) {B : {k : I} -> A k -> Set γ} {x : A i} {y : A j}
          -> (f : {k : I} -> (x : A k) -> B x)
          -> i ≅ j
          -> x ≅ y
          -> f x ≅ f y
    icong A f = cong₂ (λ _ -> f)

However `icong' has its own semantics, and it's much easier to me to parse

    icong AgdaReallyRequiresThis someFunction
something-equals-something something-equals-something

than

    cong₂ {A = AgdaReallyRequiresThis} (λ _ -> someFunction)
something-equals-something something-equals-something

2015-01-05 13:12 GMT+03:00, Helmut Grohne <grohne at cs.uni-bonn.de>:
> On Thu, Dec 18, 2014 at 12:33:26AM +0200, Andreas Abel wrote:
>> This would mean that the above definition of i-cong can be taken?!
>
> After reading the subthread started by Conor McBride I now realize that
> i-cong is indeed a special case of cong₂. To verify this, I went through
> all of my code an replaced all uses of i-cong without any problems.
> Thus, I believe and agree that i-cong is in fact not needed. I note
> however, that when using cong₂, I still had to make a few implicit
> parameters explicit to make Agda 2.4.2.2 happy.
>
> Thanks for the explanations!
>
> Helmut
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>