Author Archives: Guillaume Brunerie

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