From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:d0ca:: with SMTP id u10-v6mr2686085edo.4.1528992105326; Thu, 14 Jun 2018 09:01:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:d0d5:: with SMTP id u21-v6ls3196926edo.5.gmail; Thu, 14 Jun 2018 09:01:44 -0700 (PDT) X-Received: by 2002:aa7:c0cd:: with SMTP id j13-v6mr2670973edp.12.1528992104346; Thu, 14 Jun 2018 09:01:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528992104; cv=none; d=google.com; s=arc-20160816; b=x6N0D6Y3d1FXs84MpwTsaQHNWIiBrPRLoreWEV6hHAnm/0qazWThtkPzKrtrl0UUcs hKrUzO3bRHOXnEB50VHjfk8xG90CMkwVmRryKG4FK9Sn6KtMPuoDWWMiuYl2wKrcrzuO f9TWKuM5d+ACifIxnbhbtQRc5aqDtKD5sUv1SEb7DY+jTS2d0OS+WCZSkxAR9057XTpK U4PgWpnhuk7tXEYO6+UlvF9fI1rvX98i1rdBGh7tjgNDMHJFOf2hwnIvDpyJr3Ymu7mf 0Ma8uMOZD12E6rDJQeQjzX5Jmafya+egfirkN7GMvt1Nk4qt1uuZ4y8YbAdx1BkAC3AC 5k6w== 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=BvV/k2nyJ7Sx5KENDiHfVhMCUPG+t3N8VJsivzSMb38=; b=kmCChKfuWxLI7nB81hK40YzI379yVQpcsGu4qbd5HNUwP3R1nh09HIIMj8hyf8MR+c pMjkR+U89AFeydHaeLcndQecMmzQjRonaPbPmoE7ShZTaSpuNqSU6EBktiBb1L6rAHzS Y8dVGj3G6JGM+MU/6k6Ifayc6LA91++Gn9J9a5yKoDZmrxZ0685aePsT3yECLy+diIuA /lUFUJbQ5L5LfZsCs+ZrndOljM5pHjG6VBnLoaqV33k1fMA0aV7nC27qcuZkbRyr9ijc p0M7c+bdmgFqKfmN6xAGO45/jWsU9QfGjyI5JXC1SUceKO0Xp2ZCE5wdi11lZP9SfF4l 9ZPw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=HK3KcNGe; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22b 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-wm0-x22b.google.com (mail-wm0-x22b.google.com. [2a00:1450:400c:c09::22b]) by gmr-mx.google.com with ESMTPS id k6-v6si202421edn.1.2018.06.14.09.01.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 09:01:44 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22b as permitted sender) client-ip=2a00:1450:400c:c09::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=HK3KcNGe; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22b as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-wm0-x22b.google.com with SMTP id 69-v6so12964303wmf.3 for ; Thu, 14 Jun 2018 09:01:44 -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=BvV/k2nyJ7Sx5KENDiHfVhMCUPG+t3N8VJsivzSMb38=; b=HK3KcNGeiOKEjOOY2s6+7tYnfwKOexPozuMVkNifRfPoGELOF+njgkHFNZbqgqruZw vYJoGTORxAf22iCoWXjerMajVUdA9l6O1guFg2DhdtuPzd8pFQe+S57mSWAofxak2M32 GFj5acc/DFt7GuLm2ME6wDGRqGnYVOkeRcDogDHpjZPsWGY7aWLv+D0WCdfa/rcCty6T a3d1GT1PD99CNbzguhhj/FnxLXrAgYThySqpRytX6aJfub4Wh8k65kZBbcB8ppDmcLjU aYlwgtsfux5lUYanLTdkrjbWW8GkhMUtvfgBqaF45KrP1ckhzXJNvKEMko4FhCMMjR4t NJSA== X-Gm-Message-State: APt69E1iBDBQwP9LW+pbYtrvurKfs0384OXpqdwrgxPNWQa+/B3do7/u XprB6LI2b+m2TYrCIgeLX51g5SAMvdM= X-Received: by 2002:a1c:8fd5:: with SMTP id r204-v6mr2528923wmd.77.1528992103987; Thu, 14 Jun 2018 09:01:43 -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 m10-v6sm7022891wrq.56.2018.06.14.09.01.42 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 09:01:43 -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 18:01:41 +0200 Cc: Christian Sattler , 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 5:47 PM, Michael Shulman wrote: >=20 > Okay, if the non-algebraic wfs's are cofibrantly generated in the > traditional sense, then the model category is indeed combinatorial. > Christian has also pointed out by private email that for a locally > presentable, locally cartesian closed (oo,1)-category (and, I think, > even any cocomplete locally cartesian closed one) the infinitary > aspects of the Giraud exactness axioms follow from finitary ones (for > roughly the same reasons as in the 1-categorical case) --- > specifically the "van Kampen" nature of pushouts, which should be > provable in any elementary (oo,1)-topos and thus presumably in > cartesian cubical sets. >=20 > So it seems that it's my possibility (3) that holds -- this model > structure does present a Grothendieck (oo,1)-topos. We should be able > to work out a more traditional description of it as a left exact > localization of some (oo,1)-presheaf category by tracing through the > proofs of the presentation theorem and Giraud's theorem. >=20 a formidable task =E2=80=A6 and a good open problem! thanks for clarifying. Steve >=20 > On Thu, Jun 14, 2018 at 6:44 AM, Steve Awodey wrote: >> Ok, I think I see what you are saying: >>=20 >> we can generate an *algebraic wfs* using the generators I gave previousl= y >> (regarded as a *category*, with pullback squares of monos, etc., as arro= ws), >> and then take the underlying (non-algebraic) wfs by closing under retrac= ts, >> as usual, and the result is then cofibrantly generated by the *set* of m= aps >> you are describing, which consists of quotients of the original ones. >>=20 >> generators aside, the cofibrations are all the monos, and the fibrations >> have the RLP w/resp. to all push-out products m xo d : U >=E2=80=94> B x= I, where m >> : A >=E2=80=94> B is any mono, j : B =E2=80=94> I is some indexing makin= g m an I-indexed >> family of monos, d : I =E2=80=94> I x I is regarded as a generic point o= f I over I, >> and the pushout-product >>=20 >> m xo d : I^n +_A (A x I) >=E2=80=94> B x I >>=20 >> is formed over I as previously described. >>=20 >> yes? >>=20 >> Steve >>=20 >>=20 >> On Jun 14, 2018, at 12:27 PM, Steve Awodey wrote: >>=20 >>=20 >>=20 >> On Jun 14, 2018, at 11:58 AM, Christian Sattler >> wrote: >>=20 >> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey wrote: >>>=20 >>> but they are cofibrantly generated: >>>=20 >>> - the cofibrations can be taken to be all monos (say), which are genera= ted >>> 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)= for >>> 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. >>=20 >>=20 >> Those would be the objects of a category of algebraic generators. For >> generators of the underlying weak factorization systems, one would take = any >> cellular model S of monomorphisms, here for example =E2=88=82=E2=96=A1= =E2=81=BF/G =E2=86=92 =E2=96=A1=E2=81=BF/G where G =E2=8A=86 >> Aut(=E2=96=A1=E2=81=BF) and =E2=88=82=E2=96=A1=E2=81=BF denotes the maxi= mal no-trivial subobject, >>=20 >>=20 >> this determines the same class of cofibrations as simply taking *all* >> subobjects of representables, which is already a set. There is no reaso= n to >> act by Aut(n), etc., here. >>=20 >> and for trivial cofibrations the corresponding generators =CE=A3_I (S_{/= I} >> hat(=C3=97)_{/I} d) with d : I =E2=86=92 I=C2=B2 the diagonal (seen as l= iving over I), i.e. >> =E2=96=A1=E2=81=BF/G +_{=E2=88=82=E2=96=A1=E2=81=BF/G} I =C3=97 =E2=88= =82=E2=96=A1=E2=81=BF/G =E2=86=92 I =C3=97 =E2=96=A1=E2=81=BF/G for all n, = G, and =E2=96=A1=E2=81=BF/G =E2=86=92 I. >>=20 >>=20 >> sorry, I can=E2=80=99t read your notation. >>=20 >> the generating trivial cofibrations I stated are the following: >>=20 >> take any =E2=80=9Cindexing=E2=80=9D map j : I^n =E2=80=94> I and a mono = m : A >=E2=80=94> I^n, which we can >> also regard as a mono over I by composition with j. Over I we also have= the >> generic point d : I =E2=80=94> I x I , so we can make a push-out product= of d and m >> over I , say m xo d : U >=E2=80=94> I^n x I . Then we forget the indexi= ng over I to >> end up with the description I already gave, namely: >>=20 >> U =3D I^n +_A (A x I) >>=20 >> where the indexing j is built into the pushout over A. >>=20 >> A more direct description is this: >>=20 >> let h : I^n =E2=80=94> I^n x I be the graph of j, >> let g : A =E2=80=94> A x I be the graph of j.m, >> there is a commutative square: >>=20 >> g >> A =E2=80=94=E2=80=94 > A x I >> | | >> m | | m x I >> | | >> v v >> I^n =E2=80=94=E2=80=94> I^n x I >> | h >> j | >> v >> I >>=20 >> put the usual pushout U =3D I^n +_A (A x I) inside it, >> and the comprison map U =E2=80=94> I^n x I is the m xo d mentioned above= . >>=20 >> Steve >>=20 >>=20 >>=20 >>=20 >>=20 >>=20 >>>=20 >>> Steve >>>=20 >>>>=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 >>>>=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 >>>>>> wrote: >>>>>>=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 c= an >>>>>>> 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 o= f >>>>>>> type >>>>>>> theory with universes >>>>>>> (and conversely the fact that we have a fibrant universe is a cruci= al >>>>>>> component in the proof >>>>>>> that we have a model structure). >>>>>>>=20 >>>>>>> I described essentially the same argument for factorisation in a >>>>>>> message >>>>>>> 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 >>>>>>> framework >>>>>>> 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 cubic= al >>>>>>> sets >>>>>>> (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 >>>>>>>=20 >>>>>>> (2) the geometric realisation map is -not- a Quillen equivalence. >>>>>>>=20 >>>>>>> I believe that this result should be relevant even for people >>>>>>> interested 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= ) >>>>>>> but we >>>>>>> cannot show this in >>>>>>> cartesian cubical type theory. >>>>>>>=20 >>>>>>> It is thus important to understand better what is going on, and thi= s >>>>>>> is why >>>>>>> I post this note, >>>>>>> The point (2) is only a concrete description of Sattler=E2=80=99s a= rgument 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. >>>>>>>=20 >>>>>>> Note that this implies that the canonical map Cartesian cubes -> >>>>>>> Dedekind >>>>>>> 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 >>>>>>> structure >>>>>>> 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 >>>>>>> discussions >>>>>>> about this last week in Bonn. >>>>>>>=20 >>>>>>> -- >>>>>>> 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. >>>>>>=20 >>>>>> -- >>>>>> 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, se= nd >>>>>> an email to HomotopyTypeThe...@googlegroups.com. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>=20 >>>=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 >>=20 >>=20 >> -- >> 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. >>=20 >>=20 >>=20 >> -- >> 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. >>=20 >>=20 >> -- >> 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.