The type of 2-element types

As an application of the previous post on characterizing the identity types of a type, let us show that for a type $latex X$ which is merely equal to the type $latex \mathbf{2}$ of booleans, to show that $latex \mathbf{2}={}X$ it is equivalent to provide a point in $latex X$. Intuitively, by giving a point in $latex … Continue reading The type of 2-element types


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