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

[Andreas Abel]

But 'cons' is certainly injective, is it?  I think you overlooked the 
double-colon...

On 17.01.2014 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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/