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

# 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

# Characterizing identity types

In homotopy type theory we often need to characterize the identity type or the loop space of a given type. There is a variety of techniques to do this, but I find myself using one particular technique the most (by far). Occasionally I find myself in a situation where I need to explain this, so I … Continue reading Characterizing identity types

# 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?

# Reflexive graph quotients are pushouts

I'd like to tell about a theorem that has been useful for me on several occasions, that was also the first topic in a series of presentations I'm currently giving at the CMU HoTT seminar. It characterizes the reflexive graph quotients as a certain pushout, so it allows us to find new, possibly more intuitive descriptions … Continue reading Reflexive graph quotients are pushouts

# 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