The coinductive type generated by the universal bundle of a pointed connected type

The simplest kind of coinductive types are described by containers. Recall that a container is just a type $latex A$ with a type family $latex B : A \to{}U$. In this blog post, we will go in detail through an example of such a coinductive type, which we naturally get in the setting of homotopy … Continue reading The coinductive type generated by the universal bundle of a pointed connected type

Advertisements

Formalizing the graph model of type theory, part 3

In the induction principle for the graph quotient $latex \mathsf{colim}(\Gamma)$, we have seen that terms of a type family $latex P : \mathsf{colim}(\Gamma)\to\mathsf{Type}$ are equivalently described by terms of the transposed family $latex \Delta(P)\circ\eta$ of graphs over $latex \Gamma$. This family is no ordinary family, and in this post I'd like to discuss its special … Continue reading Formalizing the graph model of type theory, part 3

Formalizing the graph model of type theory, part 2

The most basic construction of higher inductive types can be formulated as a 'left adjoint' to the canonical homomorphism of models $latex \Delta : U \to \mathsf{Graph}$, and my interest in formalizing the graph model originates from this idea. Also, looking at the higher inductive types in this type theoretical framework has helped me prove … Continue reading Formalizing the graph model of type theory, part 2

Five stages of accepting constructive mathematics

During the special year on the Univalent foundations for mathematics at the Institute for Advanced Study, Andrej Bauer gave a talk on the Five stages of accepting constructive mathematics. In it, he compared the process a classically trained mathematician might go through (or might get stuck in) in accepting constructive mathematics, to the five stages identified by Elisabeth … Continue reading Five stages of accepting constructive mathematics

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