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.