Author Archives: Egbert Rijke

Type theoretic replacement & the n-truncation

This post is to announce a new article that I recently uploaded to the arxiv: The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in … Continue reading

Posted in Uncategorized | Leave a comment

A master thesis on homotopy type theory

In the last year, I have written my master thesis on homotopy type theory under supervision of Andrej Bauer in Ljubljana, to whom I went on an exchange, and Jaap van Oosten and Benno van den Berg in Utrecht. Their … Continue reading

Posted in Paper | 8 Comments

A type theoretical Yoneda lemma

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