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: https://arxiv.org/abs/1701.07538 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
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
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
Homotopy Type Theory 