From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a0c:ba11:: with SMTP id w17-v6mr1538709qvf.18.1528991292777; Thu, 14 Jun 2018 08:48:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:d8f5:: with SMTP id w50-v6ls3042250qvj.0.gmail; Thu, 14 Jun 2018 08:48:12 -0700 (PDT) X-Received: by 2002:a0c:cdcc:: with SMTP id a12-v6mr1505662qvn.44.1528991292062; Thu, 14 Jun 2018 08:48:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528991292; cv=none; d=google.com; s=arc-20160816; b=UpsRtrMBeFxCSGe6Hj/fWnr4PtEQsZxUdSuv1XuBZiPUgraEd/5kAUNzO6Ur0D20iN jVF51PCGS21tvmvMtj8hMmWLroWsxTZiU2ZZaPk27SpI0m/nUxjx051cNkOZukcbJtyV bK0/h2V6xoXM9FUFn5b35ERl6X7b4h8DzMqxSGCroTfSZz2P47g5x8Ic7p9A3p+ILCRX dpxZjll7a2fCFISs5Hiifkkd8aVmNRbHxR3pHLWj703olXm0dcBnP9QL7imzB1tmglrU Y2e+fln2004cbPLG4f+UlSRUuposrt4Iq00BJiazH7RQ0kyrhx6yuSmyaYWsNpf0aEEq ZNSg== 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=3rSNb0r2BGT3QP+sCz+1ztZw6ClN165/6Dy81yP4eOc=; b=kwFCtimZZwF9IH/YZycyyDvMdVtPkJpFQFMKowHnG20VUbbWHeq8DFpFwZR8biIwHH 683QwyRiPdprjk9aXiBLni0EUo1LY7usNkkL4dSUNxM/in1isTs/XinNBnv8tCXi8pst whS/+grT5+nKifG6G7nppHkkosS/ZTFo1U7uDni5C6jC+lk25pMgwLU2FA/Q/0hyCR7S 9XChK9EasFVt/Jlwz+oYlOSZtxRWZzrYarUKKTxxuKmwvIhIhcyOO5LsciaDtsnY6yMF /fBJ3bHbpwrtsjgmhFFHySAcM3q2ZR1ABb/PdEDSLBFSWo9n3sKrQ5V56GZZ6aoAtjrX L83A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ijnTougj; spf=neutral (google.com: 2607:f8b0:4002:c09::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22e.google.com (mail-yb0-x22e.google.com. [2607:f8b0:4002:c09::22e]) by gmr-mx.google.com with ESMTPS id z5-v6si347971qto.0.2018.06.14.08.48.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 08:48:11 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22e is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ijnTougj; spf=neutral (google.com: 2607:f8b0:4002:c09::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22e.google.com with SMTP id m137-v6so2396752ybm.6 for ; Thu, 14 Jun 2018 08:48:11 -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=3rSNb0r2BGT3QP+sCz+1ztZw6ClN165/6Dy81yP4eOc=; b=ijnTougjtqRSR8e2iclMoO7nelld71xIu0OeGI4WI9yGnyt9dcP0DYbktpm7ioLLP0 fd7U2UY+pt1bP472j1aAAf0V3smTGKWYsTiLX453waO+bxZ8ajeG6Wvg7B+OzuCdftOT zYoG2QKLiPbA3fWPKcGvCU2XQPtJ4oUWTnMEieYH1KovgFl5zLt29CUbZaeJL9QqpjqM rKKWxSWoAxmxRyHuM7YlkpDZ4YKesW5XPZ3nYGuhiBqaumH+6OiaWfdJMTbRKVXsabNS 9v6hsSz74ugPz+/0gIFTs63nqk+SVKYzFfYWoxmPaTkWzvbcqv2eCI5JLctVBKZ8QRow +kZw== X-Gm-Message-State: APt69E2vDtcCfshvV+0AnKVWmZPGjDVpZdiDukYZ/dw8l8i4eo2leAqV cZENzoswu4tDJGcPiQreOH8Fz0co X-Received: by 2002:a25:55d4:: with SMTP id j203-v6mr1693719ybb.199.1528991291533; Thu, 14 Jun 2018 08:48:11 -0700 (PDT) Return-Path: Received: from mail-yb0-f170.google.com (mail-yb0-f170.google.com. [209.85.213.170]) by smtp.gmail.com with ESMTPSA id l6-v6sm1378495ywd.58.2018.06.14.08.48.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 08:48:10 -0700 (PDT) Received: by mail-yb0-f170.google.com with SMTP id v17-v6so2399636ybe.7 for ; Thu, 14 Jun 2018 08:48:10 -0700 (PDT) X-Received: by 2002:a25:db46:: with SMTP id g67-v6mr1666346ybf.387.1528991290268; Thu, 14 Jun 2018 08:48:10 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Thu, 14 Jun 2018 08:47:49 -0700 (PDT) In-Reply-To: References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> From: Michael Shulman Date: Thu, 14 Jun 2018 08:47:49 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Quillen model structure To: Steve Awodey Cc: Christian Sattler , Thierry Coquand , Homotopy Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. 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. On Thu, Jun 14, 2018 at 6:44 AM, Steve Awodey wrote: > Ok, I think I see what you are saying: > > we can generate an *algebraic wfs* using the generators I gave previously > (regarded as a *category*, with pullback squares of monos, etc., as arrow= s), > and then take the underlying (non-algebraic) wfs by closing under retract= s, > as usual, and the result is then cofibrantly generated by the *set* of ma= ps > you are describing, which consists of quotients of the original ones. > > 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 making= m an I-indexed > family of monos, d : I =E2=80=94> I x I is regarded as a generic point of= I over I, > and the pushout-product > > m xo d : I^n +_A (A x I) >=E2=80=94> B x I > > is formed over I as previously described. > > yes? > > Steve > > > On Jun 14, 2018, at 12:27 PM, Steve Awodey wrote: > > > > On Jun 14, 2018, at 11:58 AM, Christian Sattler > wrote: > > On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey wrote: >> >> but they are cofibrantly generated: >> >> - the cofibrations can be taken to be all monos (say), which are generat= ed >> by subobjects of cubes as usual, and >> >> - 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. > > > Those would be the objects of a category of algebraic generators. For > generators of the underlying weak factorization systems, one would take a= ny > 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 maxim= al no-trivial subobject, > > > this determines the same class of cofibrations as simply taking *all* > subobjects of representables, which is already a set. There is no reason= to > act by Aut(n), etc., here. > > 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 li= ving 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. > > > sorry, I can=E2=80=99t read your notation. > > the generating trivial cofibrations I stated are the following: > > 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 indexin= g over I to > end up with the description I already gave, namely: > > U =3D I^n +_A (A x I) > > where the indexing j is built into the pushout over A. > > A more direct description is this: > > 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: > > 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 > > 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. > > Steve > > > > > > >> >> Steve >> >> > >> > 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 >> >>> wrote: >> >>> >> >>> 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 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). >> >>>> >> >>>> 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 >> >>>> >> >>>> https://arxiv.org/abs/1802.07588 >> >>>> >> >>>> >> >>>> >> >>>> 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 >> >>>> >> >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >> >>>> >> >>>> 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. >> >>>> >> >>>> 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. >> >>>> >> >>>> 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 >> >>>> >> >>>> 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 >> >>>> discussions >> >>>> about this last week in Bonn. >> >>>> >> >>>> -- >> >>>> 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. >> >>> >> >>> -- >> >>> 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. >> >> >> >> -- >> 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. > > > > -- > 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. > > > > -- > 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. > > > -- > 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.