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

[Jason Gross]

An arbitrary type.  For example, we can have List (Bool * Bool) = List Bool
by univalence, but Bool * Bool != Bool.  But this was based on a
mis-reading; the original proposal was to make _::_ injective, not List.

-Jason


On Sat, Jan 18, 2014 at 9:41 PM, Vladimir Voevodsky <vladimir at ias.edu>wrote:

>
> On Jan 17, 2014, at 9:31 PM, Altenkirch Thorsten <
> psztxa at exmail.nottingham.ac.uk> wrote:
>
> > Injectivity for List or Vec is not compatible with univalence. Because
> List T = List Bool but not T = Bool.
>
>
> What is T?
>
> V.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140118/f44d5f29/attachment.html