# Monthly Archives: September 2012

## 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

## Truncations and truncated higher inductive types

Truncation is a homotopy-theoretic construction that given a space and an integer n returns an n-truncated space together with a map in an universal way. More precisely, if i is the inclusion of n-truncated spaces into spaces, then n-truncation is … Continue reading

Posted in Code, Higher Inductive Types | 15 Comments