associativity for vectors

[sergey-goncharov]

Unclear, why it was not there. But it is provable.

[MatthewDaggitt]

Unclear, why it was not there.

Nothing is there until someone adds it!

Thanks, looks like a great addition. In addition to the formatting, please could you add a corresponding entry to the CHANGELOG.md file?

[sergey-goncharov]

Nothing is there until someone adds it!

Right. I've been unsure, if there are any reasons for not having it there. Incidentally https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Properties/WithK.agda contains a different proof under K, which confused me, because I nearly though that K is needed for associativity.

[MatthewDaggitt]

Incidentally https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Properties/WithK.agda contains a different proof under K, which confused me, because I nearly though that K is needed for associativity.

So the difference is that the proof under WithK is for (heterogeneous) propositional equality, whereas you have proved it for pointwise equality which is a slightly weaker notion. You haven't proved the results are equal, you've proved that all the elements are equal.

[sergey-goncharov]

Incidentally https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Properties/WithK.agda contains a different proof under K, which confused me, because I nearly though that K is needed for associativity.

So the difference is that the proof under WithK is for (heterogeneous) propositional equality, whereas you have proved it for pointwise equality which is a slightly weaker notion. You haven't proved the results are equal, you've proved that all the elements are equal.

OK, I am seeing it now. Ineed, I've been just assuming that the pointwise equality is the only desirable notion of equality for vectors, but yes, propositional equality always remains a (potentially problematic) alternative. Thank you for clarification!

[MatthewDaggitt]

Thanks, I'm marking this as done, but we're currently having issues with the test suite so I won't merge it in until we resolve that, apologies.