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

Vladimir Voevodsky vladimir at ias.edu
Sun Jan 19 03:41:47 CET 2014


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.



More information about the Agda mailing list