Hi Andrej! I think from various points of view people have already looked at this question, at least for finite limits and colimits. For instance, the 3x3-lemma states that pushouts commute with pushouts. Then one can show by the 3x3 lemma that reflexive coequalizers commute with reflexive coequalizers, because a reflexive coequalizers is just the pushouts of the source and target maps of the relation. The case of coequalizers is then obtained from the case of reflexive coequalizer by freely adding reflexivity to the relation. There also exist higher dimensional analogues of the 3x3-lemma. For instance, imagine a diagram of the shape of a 3-cube (with of course a homotopy filling the cube). There is a notion of being a cocartesian 3-cube, where the "terminal" object of the cube satisfies a universal property with respect to the rest of the cube. Then one can show that cocartesian 3 is an iterated pushout, and use this to obtain a higher dimensional 3x3-lemma for cubes, a higher dimensional descent theorem, and so on. This works for all n (as described for instance in Munson and Volic, Cubical homotopy theory, where they also derive a Blakers-Massey theorem for arbitrary dimensional cubes), but to express this in type theory one runs in to the problem of defining (semi-)simplical objects in type theory. It turns out that one can obtain the 3x3-lemma just by rotating a higher cocartesian cube (which remains cocartensian after rotation). So by studying "higher higher inductive types" one gets results about commutativity of colimits with each other. Best wishes, Egbert On Tue, Mar 13, 2018 at 1:24 PM, Andrej Bauer wrote: > In HoTT we know how to treat limits and colimits over graphs (where we > do not truncate in any way) as HITs. > > Has anyone proved in HoTT, or attempted to prove, that colimits > commute with colimits, or that limits commute with limits? My > higher-categorical mojo is non-existent, so I don't even know whether > I should expect horrible complications. But it would be quite useful > to know whether such commutativity holds. > > With kind regards, > > Andrej > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- egbertrijke.com