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