[Agda] [PATCH] add a ∷-injective for Vec like there is one for List

[Twan van Laarhoven]

This is about injectivity for the data constructor _∷_, not injectivity for the 
type constructor List or Vec.

On 17/01/14 14:31, Altenkirch Thorsten wrote:
> Injectivity for List or Vec is not compatible with univalence. Because List T
> = List Bool but not T = Bool.
>
> T.
>
> Sent from my iPhone
>
>> On 17 Jan 2014, at 12:28, "Helmut Grohne" <grohne at cs.uni-bonn.de> wrote:
>>
>> Hi,
>>
>> I found myself in need of injectivity of Vec._∷_ in a few places. While
>> there is a ∷-injective for List, there is none for Vec yet. I attach a
>> simple patch (in a format suitable to git am) to address this omission and
>> license it under the MIT license used for the standard library. I'd
>> appreciate if it could be merged. Thanks.
>>
>> Helmut <0001-add-a-injective-for-Vec-like-there-is-one-for-List.patch>
>> _______________________________________________ Agda mailing list
>> Agda at lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>> _______________________________________________ Agda mailing list
>> Agda at lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda