From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.159.55.50 with SMTP id z47mr660631uad.102.1520961862375;
        Tue, 13 Mar 2018 10:24:22 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.159.44.4 with SMTP id r4ls1115230uaj.4.gmail; Tue, 13 Mar 2018
 10:24:21 -0700 (PDT)
X-Received: by 10.176.66.133 with SMTP id j5mr639422uaj.120.1520961861428;
        Tue, 13 Mar 2018 10:24:21 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1520961861; cv=none;
        d=google.com; s=arc-20160816;
        b=msDey37O1zBFRVsEIBcwhCcjXfm+KQihn8VPXh0326mauLS+GAkSbmeblY7EpmddQY
         Hup+58ro/Ik9I7+RAYoh+AuN96twzcwnx4Hroo4ogtk12asHLYHEyr+pGOBwerCt173J
         FjgkL5uxBhHEluncfFPF3zgzHh/gw3T5QcHV732n7lD4H8BrJAz5NmH9Io0AZ8SpNoYV
         Z1AX/tezdsUxykO2oVYRFZcNfDaI9TEI0l0/hjAFPURZobBbaVayLA7iUio8SYJjx6P/
         6Zygqaa81NbRSAeMRX60P03b7riOONcNu1US11xX+zvIFKUPL8ns1lI1929D14jew7XT
         S7Mw==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=to:subject:message-id:date:from:mime-version:dkim-signature
         :arc-authentication-results;
        bh=FAC/O6HrJTc4jWmadmXpaWINqYUHE9Z1Gs0IliJ2TWQ=;
        b=MmcHTKKYKAAVUH+3MHu3DHiBSX+whMiy6jzEZMoyo2FQ6MLh6sJnUmWUfz18N4aD+1
         LYIy7wY/xXrzTKPMDKbNosPmbOHBGKAMAElBKgUuhXdKizHNxfiztJegdu2v71DY+ybT
         4a1ogkxPbpcqw/H8DVEbjemzROx+31VfGxdFbxSIFNSl+9eu1Ukwd+qXUvv5/XmefGwo
         KK0DwY9J6uf8gEI+kgQN0XEC7/NKiTkbNM//W6n/X381Buu32j6ZCcqrihB2MhsS0dLi
         k+LqiELxLfv99Aw43LDl0ER2ZiCyGX4sEi24LhUUncjY/RxRgyFiIlv85FRVjYWF8doH
         4qeg==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=k0c9fxIX;
       spf=neutral (google.com: 2607:f8b0:4001:c0b::234 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Return-Path: <andrej...@andrej.com>
Received: from mail-it0-x234.google.com (mail-it0-x234.google.com. [2607:f8b0:4001:c0b::234])
        by gmr-mx.google.com with ESMTPS id p187si41782vkp.5.2018.03.13.10.24.21
        for <homotopyt...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Tue, 13 Mar 2018 10:24:21 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:4001:c0b::234 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4001:c0b::234;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=k0c9fxIX;
       spf=neutral (google.com: 2607:f8b0:4001:c0b::234 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-it0-x234.google.com with SMTP id d13-v6so1091769itf.0
        for <homotopyt...@googlegroups.com>; Tue, 13 Mar 2018 10:24:21 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=andrej-com.20150623.gappssmtp.com; s=20150623;
        h=mime-version:from:date:message-id:subject:to;
        bh=FAC/O6HrJTc4jWmadmXpaWINqYUHE9Z1Gs0IliJ2TWQ=;
        b=k0c9fxIXw7b42+mPgi9c8C6gbEmCouuzS5M0XhbIRwrb7IRej0RkiDs5T9bjcLqCra
         N2iHDegxtObqcPxb6s9oSiCLU84JCqCfg76CSsSqRDD8wMqeaoRg1jDzD6uL37kMqjVq
         D59H4Fmpu8XbOVLWQlJvmRPz0J5rCumDL+JV+mGRC4hAbSjUwzeYXRwmyQnrVYT1S0PD
         zZC0W1kxJvu3bOByGzBqYsZlxTLIm8locxgYyhSrgVtl7FzfJd09iotwsvIS0cRmDy5X
         FzwUZHebieDcp5fSArNOBV/aNg2ZsNDHHY0m2b6T5qtrUMgYtzqg/uT9p1zm1Cj/R+Nk
         tIVQ==
X-Gm-Message-State: AElRT7F72fdUd4Kx9rqxtQQ/nR9hF8vuzh2tIU6vt3opmXIAeEwmZRJ6
	bRzY2afbnpiC+kmB0qxv1LnHnPCGKIPrvMh24EP55A==
X-Received: by 10.36.238.65 with SMTP id b62mr1813194iti.122.1520961860602;
 Tue, 13 Mar 2018 10:24:20 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.192.160.10 with HTTP; Tue, 13 Mar 2018 10:24:20 -0700 (PDT)
X-Originating-IP: [2001:1470:fff0:830:31f7:4659:12c1:de84]
From: Andrej Bauer <andrej...@andrej.com>
Date: Tue, 13 Mar 2018 18:24:20 +0100
Message-ID: <CAB0nkh0XFcN+aeUGiuhLwA-1kKe6z+qS=17=M5RDtFeFbSumKA@mail.gmail.com>
Subject: Do (co)limits commute with (co)limits?
To: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Content-Type: text/plain; charset="UTF-8"

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