From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:f082:: with SMTP id n2-v6mr133973wro.11.1528968488697; Thu, 14 Jun 2018 02:28:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:864a:: with SMTP id i71-v6ls1528574wmd.11.gmail; Thu, 14 Jun 2018 02:28:07 -0700 (PDT) X-Received: by 2002:a1c:e554:: with SMTP id c81-v6mr132541wmh.31.1528968487437; Thu, 14 Jun 2018 02:28:07 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528968487; cv=none; d=google.com; s=arc-20160816; b=TF3wHwRx05i8D90ffVDclb22omYQuovNmBXEBYXAOurH7MbgbdU6Q8kEme58Lt0js4 ezan3ccwc3L0sObkkL6FoTL/68XB1apQqBvrt4WLuwVi7yoE8ivmqR29TI2sYZx3pWwP TTSlv4TNzZI7L/bM1w9btTZMK24BFI2enQvIgRTGrzHCZ2yvEy4VWpYsloYWG2a+ZtLR GiV2DFFPUqDwRFDFlSb5Ks4lkAz/+UGv2E83XIwjTRiDWwfgjSIddh//C3HQSds2yJ8V GuIsJlVKh4yGTj2Fjml7Uw1IGxQiEAJ0rWCseT4D50N0oGa2/CKgvTf9ScLoLjyZC+fT 3L0g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature :arc-authentication-results; bh=6HbcWMb/rl1BrRWY77NZixFYNLI804RN/uNmQ4pkWLk=; b=LCbTK3ku0Z9ox9RpZdi9jgyHxib9DX2GlnlhR8+qRD8oXFXiw5P0GpqdPdXXpGof2H jzmnHEqPQsv1uEdvR5QfIi3xe2dKYvoFz6OzRhG7X2/NhXkkA7bY8QQvOQ4QW67SmPCL sGLzkBhYsP8PSCdFvunijIRvOmbc35P/irnYf8iSxkcGNxNNtXjVJ00sEYJ6fnHZP2TG KG4eH0lZWTCLp5AVkUUtQPNEgyKV177aL29lpuQtitw0xBsOXpWU8V7LiKq+k+vLY/QY UtWsnCpXPlDuc5hr+XmwQbwL1gFc6jyCoa1es9tunW64AyH0tF3KuanGO2tFloZxEtpA XeQw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=ecDX7tSO; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::22c as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-wr0-x22c.google.com (mail-wr0-x22c.google.com. [2a00:1450:400c:c0c::22c]) by gmr-mx.google.com with ESMTPS id c23-v6si93761wmb.0.2018.06.14.02.28.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 02:28:07 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::22c as permitted sender) client-ip=2a00:1450:400c:c0c::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=ecDX7tSO; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::22c as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-wr0-x22c.google.com with SMTP id k16-v6so5635384wro.0 for ; Thu, 14 Jun 2018 02:28:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=6HbcWMb/rl1BrRWY77NZixFYNLI804RN/uNmQ4pkWLk=; b=ecDX7tSOdJ0TMOM4KAkPxUYOkA8nhGIw4e6xgM9m2JOLoTlADIodI0NIp5M03bVUZ7 A6lykQB5SBlNVfcl3Hrv+czZSV3Tp7VCtpnQ3zqFE57evuXH9HozyX5K3D0lKy8aeII7 crVFnVrT4CDl9uLBNuj5DZDnXYLBwoiGHv/ftxf7shiWMxipPOw2C7J8tHak+03BGsk7 RCbAYTCcpjemC0OXb0sfmySV6sxDaG1xfTDrPTUQQQBFEDQKq5H3kxF6Vdz5Bbh7f9Z3 DD+LaAzQieeRXTEa9mPQcG+KPMf7STIJRs+OgC6GMZwg5ygr7CyaWexE3YXdCkd8uESX 9neg== X-Gm-Message-State: APt69E3ZUjpAZTimT+nJSchkziC8K4sIRIjTKF+332asTnXBVwY97ih0 2bt2vFEJJ1mVD32xh5vrY1DTYbs8Jxw= X-Received: by 2002:adf:c844:: with SMTP id e4-v6mr1457053wrh.236.1528968487038; Thu, 14 Jun 2018 02:28:07 -0700 (PDT) Return-Path: Received: from ?IPv6:2003:e2:af2e:8400:ec11:d9b5:73b8:ff64? (p200300E2AF2E8400EC11D9B573B8FF64.dip0.t-ipconnect.de. [2003:e2:af2e:8400:ec11:d9b5:73b8:ff64]) by smtp.gmail.com with ESMTPSA id t17-v6sm6364042wrr.82.2018.06.14.02.28.05 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 02:28:06 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 11.3 \(3445.6.18\)) Subject: Re: [HoTT] Quillen model structure From: Steve Awodey In-Reply-To: Date: Thu, 14 Jun 2018 11:28:04 +0200 Cc: Thierry Coquand , Homotopy Theory Content-Transfer-Encoding: quoted-printable Message-Id: References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> To: Michael Shulman X-Mailer: Apple Mail (2.3445.6.18) > On Jun 14, 2018, at 12:00 AM, Michael Shulman wrote= : >=20 > 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. yes, that=E2=80=99s correct. >=20 > 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: >=20 > 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. that=E2=80=99s possible, I suppose =E2=80=A6 >=20 > 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. but they are cofibrantly generated: - the cofibrations can be taken to be all monos (say), which are generated = by subobjects of cubes as usual, and=20 - the trivial cofibrations are generated by certain subobjects U >=E2=80=94= > I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) f= or all A >=E2=80=94> I^n cofibrant and there is some indexing I^n =E2=80=94= > I . In any case, a small set of generating trivial cofibrations. Steve >=20 > 3. They might be a Grothendieck (oo,1)-topos after all. >=20 > I don't know which of these is most likely; they all seem strange. >=20 >=20 >=20 >=20 > 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. >>=20 >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman wro= te: >>>=20 >>> 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? >>>=20 >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >>> wrote: >>>> The attached note contains two connected results: >>>>=20 >>>> (1) a concrete description of the trivial cofibration-fibration >>>> factorisation for cartesian >>>> cubical sets >>>>=20 >>>> It follows from this using results of section 2 of Christian Sattler= =E2=80=99s >>>> paper >>>>=20 >>>> https://arxiv.org/pdf/1704.06911 >>>>=20 >>>> that we have a model structure on cartesian cubical sets (that we can = call >>>> =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 t= ype >>>> 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). >>>>=20 >>>> 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 framew= ork >>>> in the paper of Andrew Swan >>>>=20 >>>> https://arxiv.org/abs/1802.07588 >>>>=20 >>>>=20 >>>>=20 >>>> Since there is a canonical geometric realisation of cartesian cubical = sets >>>> (realising the formal >>>> interval as the real unit interval [0,1]) a natural question is if thi= s is a >>>> Quillen equivalence. >>>> The second result, due to Christian Sattler, is that >>>>=20 >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >>>>=20 >>>> I believe that this result should be relevant even for people interest= ed in >>>> the more syntactic >>>> aspects of type theory. It implies that if we extend cartesian cubica= l 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) b= ut we >>>> cannot show this in >>>> cartesian cubical type theory. >>>>=20 >>>> It is thus important to understand better what is going on, and this i= s why >>>> I post this note, >>>> The point (2) is only a concrete description of Sattler=E2=80=99s argu= ment he >>>> presented last week at the HIM >>>> meeting. Ulrik Buchholtz has (independently) >>>> more abstract proofs of similar results (not for cartesian cubical set= s >>>> however), which should bring >>>> further lights on this question. >>>>=20 >>>> Note that this implies that the canonical map Cartesian cubes -> Ded= ekind >>>> 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 str= ucture >>>> obtained by transfer >>>> and described at >>>>=20 >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>>>=20 >>>> is not equivalent to the type-theoretic model structure. >>>>=20 >>>> Thierry >>>>=20 >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discuss= ions >>>> about this last week in Bonn. >>>>=20 >>>> -- >>>> You received this message because you are subscribed to the Google Gro= ups >>>> "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. >>>=20 >>> -- >>> 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. >>=20