A hierarchy of ∞-equivalence relations

We have seen what kind of structure the structure of an ∞-equivalence relation is. Now it is time to describe some classes of examples. Of course, once you've shown that your notion of equivalence relation meets the two requirements, then you have an exhaustive class of examples: the kernels of maps. Nevertheless, there are some classes of … Continue reading A hierarchy of ∞-equivalence relations

What kind of structure is the structure of an ∞-equivalence relation?

Suppose you have come up with a certain extra structure, formulated in homotopy type theory, that a binary type-valued relation $latex R$ on $latex A$ may possess, and you'd like to say that it is an ∞-equivalence relation. Well, then you have to show that it is one! In this post I'd like to give … Continue reading What kind of structure is the structure of an ∞-equivalence relation?

What I learned this summer about coinductive types

This summer I did research at Inria Nantes with the people in the CoqHoTT group, in particular with Nicolas Tabareau and Simon Boulier. Specifically, we worked on a coinductive approach to $latex \infty$-equivalence relations, about which I'll give a talk tomorrow at the CMU HoTT seminar. Thus, I had to learn how to handle coinductive … Continue reading What I learned this summer about coinductive types