Monthly Archives: May 2012

Reducing all HIT’s to 1-HIT’s

Posted on 7 May 2012 by Peter LeFanu Lumsdaine

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

A type theoretical Yoneda lemma

Posted on 2 May 2012 by Egbert Rijke

In this blog post I would like to approach dependendent types from a presheaf point of view. This allows us to take the theory of presheaves as an inspiration for results in homotopy type theory. The first result from this … Continue reading →

Posted in Foundations | 2 Comments