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

[Altenkirch Thorsten]

Oops sorry :-(

Sent from my iPhone

> On 17 Jan 2014, at 14:40, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:
> 
> 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/