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

[Altenkirch Thorsten]

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