Author Archives: Peter LeFanu Lumsdaine

Reducing all HIT’s to 1-HIT’s

For a while, Mike Shulman and I (and others) have wondered on and off whether it might be possible to represent all higher inductive types (i.e. with constructors of arbitrary dimension) using just 1-HIT’s (0- and 1-cell constructors only), somewhat … Continue reading

Posted in Higher Inductive Types | 5 Comments

Strong functional extensionality from weak

It’s amazing what you can find in the HoTT repository these days! I was browsing it the other week, looking up something quite different, when I came across a theorem in Funext.v (originally by Voevodsky) which answers, in a surprising … Continue reading

Posted in Uncategorized | 5 Comments

Higher Inductive Types: a tour of the menagerie

(This was written in inadvertent parallel with Mike’s latest post at the Café, so there’s a little overlap — Mike’s discusses the homotopy-theoretic aspects more, this post the type-theoretic nitty-gritty.) Higher inductive types have been mentioned now in several other … Continue reading

Posted in Code, Higher Inductive Types | 8 Comments