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 , is the join of 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 consisting of a type of vertices, a binary type-valued relation of edges, and a proof of reflexivity . A morphism of reflexive graphs is similarly a triple consisting of a action on vertices , an action on edges , with witnessing that reflexivity is preserved.
For any type we have the discrete reflexive graph . The operation 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 to be the left adjoint to , we can introduce it accordingly. The type is going to be a higher inductive type, and the constructors of are going to assemble the unit of our adjunction. Thus, we have a morphism of reflexive graphs. The induction principle for will tell us how to construct a section of a dependent type . In other words, it will tell us how to construct a lift
Since we want an adjunction, it should suffice to find a lift in the transposed diagram
Thus, we formulate the induction principle for as follows: to construct a section of , it suffices to construct a lift of in the reflexive graph model, along the indicated projection. The computation rule then says that the resulting section will satisfy . It turns out that these requirements suffice to prove the desired universal property for . On to the theorem!
Theorem 1. Let be a reflexive graph with reflexive graph quotient . Then the square
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 -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 is the join , since the total space of the binary relation is just .
Recall that Van Doorn uses the indiscrete (non-reflexive) graph to construct the propositional truncation. More precisely, he shows that the sequential colimit of operations 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 of iterated join powers of a type with itself. Let us consider the subsequence , which has the same colimit. Since the join is an associative operation, it follows that the . By our observation that , it follows that this sequence is just the sequence . 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 is left adjoint to the discrete functor . There is also a right adjoint to , which just returns the type of vertices of a reflexive graph. Furthermore, the indiscrete functor 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 () followed by the left-most (). This leaves us with the question whether we get something similar in other cohesive (-)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 -toposes.