From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a6b:2352:: with SMTP id j79-v6mr2908387ioj.127.1528927230438; Wed, 13 Jun 2018 15:00:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:b719:: with SMTP id h25-v6ls70231itf.10.gmail; Wed, 13 Jun 2018 15:00:29 -0700 (PDT) X-Received: by 2002:a24:f002:: with SMTP id s2-v6mr3052580ith.52.1528927229851; Wed, 13 Jun 2018 15:00:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528927229; cv=none; d=google.com; s=arc-20160816; b=XhlWpb5BjtPiXfj8D+5VKxjW/JFo4YQ0mSKvMea9qtX6Dj1j9FceVQG73XJdCeFVLP QYH/LQPPAQDc6VmY7tNxpyeDUfks3E/bA6t+otwFqJ31RUHwMVyyBH9MV18IeKLleC77 cti1CznhN+v7A+c6uOq9bOa2llqxLBEktmNo0fICxUPZzwvPlhFZYnX+7cvx1uI5FhN9 ay+MjC8R8qM9D7FvjRtxq6wD5i1mJ5hZsH+JwXLIqYYoWR5kJKLMaag0yktiZWizSjQT HcjjFTb04WKbyUgMkygploX9+clQfdhxBHx6M+7sHsgdOXXZ10nt2sx3Qe23Nkup0u+Y M3lw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=I86hGHdcDbOWcBTfSlFJhhEi4jYVA2i6RiJ4nqFTxJY=; b=JgaJwMJ0o8Ghq+jtMbPvvyawzYxgujBxrNwoH3CVGY6T/keRLnXnyU+9gSBWhzLIaz 3cZiH8+oYhBZsYYK/iLFC0++THT+ItilEXijxnwaAM3rlN8DH4FyHbYj7ZnhWTgtJ3Y4 7a5zSWe3BrHDcPKc/bkdb/5QpLjWVTg4kGoFV1lHR+TsQG187LcOKAn31Kc+m5LPx6rS 3GJxGHW8tqRo1ZF9rur012lyoB/AW6atBHmg4hIEAUiQetifoevmBUzDAeasUVIdY4lK ElLCQ+bE9VC1rHiW675fs8RO55TvQEqQlgTHWyMH5JgE3u8iiTnRFqac/FWyahIt3kcJ 5tGw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=YQMZcA+b; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x230.google.com (mail-yw0-x230.google.com. [2607:f8b0:4002:c05::230]) by gmr-mx.google.com with ESMTPS id h17-v6si6298itj.4.2018.06.13.15.00.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Jun 2018 15:00:29 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=YQMZcA+b; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x230.google.com with SMTP id v197-v6so1424463ywc.13 for ; Wed, 13 Jun 2018 15:00:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=I86hGHdcDbOWcBTfSlFJhhEi4jYVA2i6RiJ4nqFTxJY=; b=YQMZcA+bHScUKXT8k6xub3ulxX39dFoHC23jnfak0/TOjYUKTjwXH4cmZygsxgvzdT wMrHfN/yTV1sjCCMZ6qJJWyr/Fyy8r2ETOEkPFOXdnCMjVS5eMyqSX52b6/O3hcMlteA P+wk13mRR4LxUIeZRQBhzkrcg/7p911wjf0uyF/RKOEhbQiy2OKwD8k1Axs9QCzINdH4 gjZD9hEynafkZ2NLbjVb/k/O8cKFL0FJSPCA9jWgCk+8WW1U7OrJd5gD1ZBqv7j3lf8X 7gITrLX48QdlWhwwju9ijyO97JhCnoARLUcHgZqiThGnym/8qIouDeGSG+M3QNvCOgMW YA4Q== X-Gm-Message-State: APt69E1w7AP19XVWHV5t3zaYXwwTX0hT5wQ2al3h6hWRjXDC3DNaDff4 4lronG/ElXqAQQ6up2MoWP7oPPDE X-Received: by 2002:a0d:e7c5:: with SMTP id q188-v6mr3259262ywe.435.1528927229176; Wed, 13 Jun 2018 15:00:29 -0700 (PDT) Return-Path: Received: from mail-yw0-f178.google.com (mail-yw0-f178.google.com. [209.85.161.178]) by smtp.gmail.com with ESMTPSA id g11-v6sm1430720ywb.100.2018.06.13.15.00.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Jun 2018 15:00:28 -0700 (PDT) Received: by mail-yw0-f178.google.com with SMTP id k18-v6so882725ywm.11 for ; Wed, 13 Jun 2018 15:00:28 -0700 (PDT) X-Received: by 2002:a81:2c54:: with SMTP id s81-v6mr3279992yws.63.1528927227889; Wed, 13 Jun 2018 15:00:27 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Wed, 13 Jun 2018 15:00:07 -0700 (PDT) In-Reply-To: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> From: Michael Shulman Date: Wed, 13 Jun 2018 15:00:07 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Quillen model structure To: Steve Awodey Cc: Thierry Coquand , Homotopy Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable In the 1-categorical case, I believe that every locally small (co)complete elementary 1-topos is defined over Set: its global sections functor has a left adjoint by cocompleteness, and the left adjoint is left exact by the Giraud exactness properties (which hold for any (co)complete elementary 1-topos). Such a topos can only fail to be Grothendieck by lacking a small generating set. In the oo-case, certainly cartesian cubical sets present a locally small (oo,1)-category (any model category does, at least assuming its locally small as a 1-category), so it seems to me there are three possibilities: 1. Although they are presumably an "elementary (oo,1)-topos" in the finitary sense that provides semantics for HoTT with HITs and univalent universes, they might fail to satisfy some of the oo-Giraud exactness properties. Presumably they are locally cartesian closed and coproducts are disjoint, so it would have to be that not all groupoids are effective. 2. They might lack a small generating set, i.e. the (oo,1)-category might not be locally presentable. Every combinatorial model category (i.e. cofibrantly generated model structure on a locally presentable 1-category) presents a locally presentable (oo,1)-category, and the 1-category of cartesian cubical sets is certainly locally presentable, but I suppose it's not obvious whether these weak factorization systems are cofibrantly generated. 3. They might be a Grothendieck (oo,1)-topos after all. I don't know which of these is most likely; they all seem strange. On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey wrote: > oh, interesting! > because it=E2=80=99s not defined over sSet, but is covered by it. > >> On Jun 13, 2018, at 10:33 PM, Michael Shulman wrot= e: >> >> This is very interesting. Does it mean that the (oo,1)-category >> presented by this model category of cartesian cubical sets is a >> (complete and cocomplete) elementary (oo,1)-topos that is not a >> Grothendieck (oo,1)-topos? >> >> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >> wrote: >>> The attached note contains two connected results: >>> >>> (1) a concrete description of the trivial cofibration-fibration >>> factorisation for cartesian >>> cubical sets >>> >>> It follows from this using results of section 2 of Christian Sattler=E2= =80=99s >>> paper >>> >>> https://arxiv.org/pdf/1704.06911 >>> >>> that we have a model structure on cartesian cubical sets (that we can c= all >>> =E2=80=9Ctype-theoretic=E2=80=9D >>> since it is built on ideas coming from type theory), which can be done = in a >>> constructive >>> setting. The fibrant objects of this model structure form a model of ty= pe >>> theory with universes >>> (and conversely the fact that we have a fibrant universe is a crucial >>> component in the proof >>> that we have a model structure). >>> >>> I described essentially the same argument for factorisation in a messa= ge >>> to this list last year >>> July 6, 2017 (for another notion of cubical sets however): no quotient >>> operation is involved >>> in contrast with the "small object argument=E2=80=9D. >>> This kind of factorisation has been described in a more general framewo= rk >>> in the paper of Andrew Swan >>> >>> https://arxiv.org/abs/1802.07588 >>> >>> >>> >>> Since there is a canonical geometric realisation of cartesian cubical s= ets >>> (realising the formal >>> interval as the real unit interval [0,1]) a natural question is if this= is a >>> Quillen equivalence. >>> The second result, due to Christian Sattler, is that >>> >>> (2) the geometric realisation map is -not- a Quillen equivalence. >>> >>> I believe that this result should be relevant even for people intereste= d in >>> the more syntactic >>> aspects of type theory. It implies that if we extend cartesian cubical= type >>> theory >>> with a type which is a HIT built from a primitive symmetric square q(x= ,y) =3D >>> q(y,z), we get a type >>> which should be contractible (at least its geometric realisation is) bu= t we >>> cannot show this in >>> cartesian cubical type theory. >>> >>> It is thus important to understand better what is going on, and this is= why >>> I post this note, >>> The point (2) is only a concrete description of Sattler=E2=80=99s argum= ent he >>> presented last week at the HIM >>> meeting. Ulrik Buchholtz has (independently) >>> more abstract proofs of similar results (not for cartesian cubical sets >>> however), which should bring >>> further lights on this question. >>> >>> Note that this implies that the canonical map Cartesian cubes -> Dede= kind >>> cubes (corresponding >>> to distributive lattices) is also not a Quillen equivalence (for their >>> respective type theoretic model >>> structures). Hence, as noted by Steve, this implies that the model stru= cture >>> obtained by transfer >>> and described at >>> >>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>> >>> is not equivalent to the type-theoretic model structure. >>> >>> Thierry >>> >>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussi= ons >>> about this last week in Bonn. >>> >>> -- >>> You received this message because you are subscribed to the Google Grou= ps >>> "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. >> >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >