Category Archives: Paper

Modeling Univalence in Inverse Diagrams

Posted on 15 March 2012 by

I have just posted the following preprint, which presents new set-theoretic models of univalence in categories of simplicial diagrams over inverse categories (or, more generally, diagrams over inverse categories starting from any existing model of univalence). The univalence axiom for … Continue reading →

Posted in Models, Paper, Univalence | 5 Comments

Inductive Types in HoTT

Posted on 19 January 2012 by

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