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 of what certain instances of these reflexive graph quotients are. For instance, we show that the reflexive graph quotient of the indiscrete graph of a type X, is the join X\ast{} X of X with itself. This allows us to use our characterization of reflexive graphs to relate Floris van Doorn’s construction and Simon Boulier’s construction of the propositional truncation to the `join construction’ of the propositional truncation.

Recall that a reflexive graph in homotopy type theory is a triple (A,R,\rho) consisting of a type A:U of vertices, a binary type-valued relation R: A\to{} A\to{} U of edges, and a proof of reflexivity \rho:\Pi_{(x:A)}~R(x,x). A morphism of reflexive graphs (A,R,\rho)\to{}(B,S,\sigma) is similarly a triple (f,g,h) consisting of a action on vertices f : A\to{}B, an action on edges g : \Pi_{(x,y:A)}~R(x,y)\to{}S(f(x),f(y)), with h:\Pi_{(x:A)}~g(\rho(x))=\sigma(x) witnessing that reflexivity is preserved.

For any type X:U we have the discrete reflexive graph \Delta(X):=(X,\mathsf{Id}_X,\mathsf{refl}). The operation \Delta can be made into a morphism of internal models, and this blog post is about the `left adjoint’ to this morphism of internal model: the reflexive graph quotients. Since we intend \mathsf{colim} to be the left adjoint to \Delta, we can introduce it accordingly. The type \mathsf{colim}(A,R,\rho) is going to be a higher inductive type, and the constructors of \mathsf{colim}(A,R,\rho) are going to assemble the unit of our adjunction. Thus, we have a morphism \eta : (A,R,\rho)\to{}\Delta(\mathsf{colim}(A,R,\rho)) of reflexive graphs. The induction principle for \mathsf{colim}(A,R,\rho) will tell us how to construct a section of a dependent type P:\mathsf{colim}(A,R,\rho)\to{}U. In other words, it will tell us how to construct a lift

20161008_2

Since we want an adjunction, it should suffice to find a lift in the transposed diagram

20161008_3

Thus, we formulate the induction principle for \mathsf{colim}(A,R,\rho) as follows: to construct a section f of P, it suffices to construct a lift g of \Delta(P)\circ\eta in the reflexive graph model, along the indicated projection. The computation rule then says that the resulting section f will satisfy \Delta(f)\circ\eta=g. It turns out that these requirements suffice to prove the desired universal property for \mathsf{colim}(A,R,\rho). On to the theorem!

Theorem 1. Let (A,R,\rho) be a reflexive graph with reflexive graph quotient \mathsf{colim}(A,R,\rho). Then the square

20161008

is a pushout square.

This theorem has been formalized in Coq by Simon Boulier while I visited him and Nicolas Tabareau, as part of our ongoing project on a formulation of \infty-equivalence relations. The proof is by directly comparing cocones in the two situations. An immediate corollary is that the reflexive graph quotient of the indiscrete graph \nabla(X) is the join X\ast{} X, since the total space of the binary relation is just X\times X.

Recall that Van Doorn uses the indiscrete (non-reflexive) graph \nabla(X) to construct the propositional truncation. More precisely, he shows that the sequential colimit of operations (\mathsf{colim}\circ\nabla)^n is the propositional truncation. Similarly, Boulier uses the indiscrete reflexive graphs. We can now compare these constructions to the `join construction’ of the propositional truncation, where the propositional truncation is constructed as the colimit of operations ({-})^{\ast{} n} of iterated join powers of a type with itself. Let us consider the subsequence ({-})^{\ast{}2^m}, which has the same colimit. Since the join is an associative operation, it follows that the ({-})^{\ast 2^{m+1}} = ({-})^{\ast 2^m} \ast ({-})^{\ast 2^m}. By our observation that \mathsf{colim}(\nabla(X))= X\ast X, it follows that this sequence is just the sequence (\mathsf{colim}\circ\nabla)^m. In other words, Boulier’s approximating sequence of the propositional truncation appears as a subsequence of the approximating sequence that we get from the join-powers.

There one more observation that I’d like to make. As we’ve mentioned, the reflexive graph quotient \mathsf{colim} is left adjoint to the discrete functor \Delta. There is also a right adjoint to \Delta, which just returns the type of vertices of a reflexive graph. Furthermore, the indiscrete functor \nabla is right adjoint. Thus, in the setting of graphs we have obtained the reflective subuniverse of mere propositions by iteratively composing the outer two of these adjoints: the right-most (\nabla) followed by the left-most (\mathsf{colim}). This leaves us with the question whether we get something similar in other cohesive (\infty-)toposes. That’s a question I’m currently working on with Jonas Frey. I’d love to hear insights from people who are familiar with cohesive \infty-toposes.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s