Monthly Archives: January 2012

Univalence versus Extraction

From a homotopical perspective, Coq’s built-in sort Prop is like an undecided voter, wooed by both the extensional and the intensional parties. Sometimes it leans one way, sometimes the other, at times flirting with inconsistency.

Posted in Uncategorized | 18 Comments

Inductive Types in HoTT

With all the excitement about higher inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report … Continue reading

Posted in Code, Foundations, Paper | 9 Comments