Re: [HoTT] Do (co)limits commute with (co)limits?

[Egbert Rijke <e.m....@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2525 bytes --]

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 <andrej...@andrej.com>
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

[-- Attachment #2: Type: text/html, Size: 3337 bytes --]