From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.8.17 with SMTP id 17mr340949wmi.25.1521055096503; Wed, 14 Mar 2018 12:18:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.209.5 with SMTP id a5ls708873wri.3.gmail; Wed, 14 Mar 2018 12:18:15 -0700 (PDT) X-Received: by 10.223.198.1 with SMTP id n1mr69404wrg.3.1521055095208; Wed, 14 Mar 2018 12:18:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1521055095; cv=none; d=google.com; s=arc-20160816; b=zxWIAM/7MleOUnKJgP+SIInuEQc5z7ZJKNRAwtAJGCFFR7E8UTkjx7H0Fi/yJpchmN qbb95XlrwxTqwu04ItE4fd8A0sxakDo5tjPo/qPdMpNiPO2a0b9UYoC8iX6SUkB3QTKS pvGJK7SA7rgHTlpvLRa9Pnn+e8W68HU/PLOqpONqIEutKvvYyKoFN9oj71bfY7B4JvfE 9Goyxi9K0sW2JnojdRqUrxDMkP6ztKSffowfASws2h5PrXCIAElCF5K4lHfRXHP1dao7 hEBEVdEhH7iwrh1Vs8K4dHlIz7EVvPcOytOq8Ek4aNLI04CKt8o4NsPmOTYZk0ywoEaM ljIQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=mCwAesoC9ZVuQAlMn2nTfPV82d8IZQehIjORCRUzwQc=; b=MmXEm/WuNKLzOBd4wV3nyAg6Dj7DW9bUJdfivdrHYLR8XBoBkNOS9VjbQVzysGvoLd POiSeQUhBVxQ44x5OjebfzhvBCIrOp94KMnMX1wJFV1bWz+D1sFDjXZnSFwNuhtjLXTT qBwZoofxzZ9gQr8Vuiv19yAQ/78tg5jkKZ0IQeDv2yv4a1VqW6Nscl0/03mCTD4PlzpH urkJur5rQ+I/ZQ6/NXxd4dYiAiVqFhoNZ6CJorF+lcGJNxebACIJUZKJ+Y/VLqqamZin WqdJhjfiVCiZl24sYHVI9GtDnnm+Tnod2ef3OMUfobhvooqCUbLHApPgmq79Eg+WALim LOHA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ZYUj6O/Q; spf=pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c0c::22b as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr0-x22b.google.com (mail-wr0-x22b.google.com. [2a00:1450:400c:c0c::22b]) by gmr-mx.google.com with ESMTPS id a139si55467wma.4.2018.03.14.12.18.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 14 Mar 2018 12:18:15 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c0c::22b as permitted sender) client-ip=2a00:1450:400c:c0c::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ZYUj6O/Q; spf=pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c0c::22b as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wr0-x22b.google.com with SMTP id n12so5926512wra.2 for ; Wed, 14 Mar 2018 12:18:15 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=mCwAesoC9ZVuQAlMn2nTfPV82d8IZQehIjORCRUzwQc=; b=ZYUj6O/QgBWjbKeDIcknYs/E/dAQf0UJt3mN2LhwuJUg/nEVEDaYM6GGeykPSOH3Cr Zg+za9HXnbFAw1O0+IrJqEUFYY/Av3sscG9qzJfnJ7AGs7ZJDAdcx2uc7BEJw7t6vBha mh35yV/Bb0QBhILT9LZBLQ1EnxWKRfwxHgGfQHAviDOznEP8cSp0siFlSo+gZfNCJp9b leVOfV1BASjFdpLnfpuTNbyCjL3wnE5TRVuvm9jhS9vN1Fyxl72UrI7t1GajlUWUfKG3 PfysTdzTjy6xBbCDksrKgcOsVS7DB78iC3Rki4GBwh3Cgri3XTzseMmj6w7xXAweaVSB hmsg== X-Gm-Message-State: AElRT7HvhwvbibfCDgm2qZpr215hXhYBzVJ3bkYXOc8EDQ+b7rEMx8bE 8MMynGdkegTex04Gfa30DskmNfUreJAke+w9Cl0= X-Received: by 10.223.184.188 with SMTP id i57mr4910538wrf.105.1521055094653; Wed, 14 Mar 2018 12:18:14 -0700 (PDT) MIME-Version: 1.0 Received: by 10.223.178.134 with HTTP; Wed, 14 Mar 2018 12:18:14 -0700 (PDT) In-Reply-To: References: From: Egbert Rijke Date: Wed, 14 Mar 2018 15:18:14 -0400 Message-ID: Subject: Re: [HoTT] Do (co)limits commute with (co)limits? To: Andrej Bauer Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="f403045fa4c899c5a10567643cc7" --f403045fa4c899c5a10567643cc7 Content-Type: text/plain; charset="UTF-8" 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 --f403045fa4c899c5a10567643cc7 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Andrej!

I think from v= arious points of view people have already looked at this question, at least= for finite limits and colimits. For instance, the 3x3-lemma states that pu= shouts commute with pushouts. Then one can show by the 3x3 lemma that refle= xive coequalizers commute with reflexive coequalizers, because a reflexive = coequalizers is just the pushouts of the source and target maps of the rela= tion. 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 insta= nce, 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 t= he "terminal" object of the cube satisfies a universal property w= ith respect to the rest of the cube. Then one can show that cocartesian 3 i= s an iterated pushout, and use this to obtain a higher dimensional 3x3-lemm= a for cubes, a higher dimensional descent theorem, and so on.

=
This works for all n (as described for instance in Munson and Volic, C= ubical 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 t= urns out that one can obtain the 3x3-lemma just by rotating a higher cocart= esian cube (which remains cocartensian after rotation). So by studying &quo= t;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.co= m> wrote:
In HoTT we know h= ow 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.



--
--f403045fa4c899c5a10567643cc7--