Author Archives: Nils Anders Danielsson
Isomorphism implies equality
Thierry Coquand and I have proved that, for a large class of algebraic structures, isomorphism implies equality (assuming univalence). A class of algebraic structures Structures in this class consist of a type, some operations on this type, and propositional axioms … Continue reading
Posted in Applications, Code, Univalence
13 Comments
Positive h-levels are closed under W
I was asked about my proof showing that positive h-levels are closed under W (assuming extensionality), so I decided to write a short note about it. W-types are defined inductively as follows (using Agda notation): data W (A : Set) … Continue reading
Posted in Code
18 Comments
Homotopy Type Theory 