From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1f:b58c:: with SMTP id e134-v6mr763808vkf.55.1528970306422; Thu, 14 Jun 2018 02:58:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:b54c:: with SMTP id e73-v6ls478883vkf.3.gmail; Thu, 14 Jun 2018 02:58:25 -0700 (PDT) X-Received: by 2002:a1f:29ca:: with SMTP id p193-v6mr758645vkp.111.1528970305477; Thu, 14 Jun 2018 02:58:25 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528970305; cv=none; d=google.com; s=arc-20160816; b=ME5iVcXRrddSco/pEBo7nUqGVUNgv2iXINYwHTfCZJ8TY8l5IsmkUPZ4Wq5BNS/4Ot sqU1jEw2N7MfQaFetSmZsELhhQzLmGgQtLMsSOCc0V8PiHaeS5DomsXu49WjPDXm7dGs dfKU2SMBer70Lb3rNDJC2RWVXNPLUD22+PsIJLmQTzB+nx1xd+QHnHxVdhRL/EPALhqc +encKHh0xPS2m2gV2TGsOE9vz/hpmCpslkZqrPfEDUYKbFZ14FK1gPfilelR3d5+KTUh Bq9Pz9p8rl8LJwjbLlYnT5owBEaP865sxy9RECIFtrOy4vRb9e//cYfxnI/lCIPc0Kna VeyQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=PrO4HnO9ucjodyj0CYzuBrl9OXQur1HLx1NTbkw3ZpY=; b=x/O/UUAaNcQkdO/9lI7JyUq9nNhgL101G8eeV9MDIbx18uQ8OBgvljZN96afpMmtBh pLKkk1LO2vyCSHgP9RtcfL9DR4TNjqjq8mEnGpFpnd0Wsm9O7hFXxVP4+F1F3/18fQRK +j0NN9N8GNepGApRjPxwWYpR8b25atCY5SockoapNSO3CZ1NtZWFb3FUoACxefw6aBGo EL90da9yqvXSCqxf2z0fSunKAABVgoS7Hh5uPR27gaYs7d8iEYjAc4dddpCcgZikz+h6 YBNrWrGvPNZb50EYRJhMc+m2f+BPyTudeE9phoqAfivQtqwNcprKEQTMampF3HnSZVFY C+tg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ugCufGqQ; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::22c as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-pf0-x22c.google.com (mail-pf0-x22c.google.com. [2607:f8b0:400e:c00::22c]) by gmr-mx.google.com with ESMTPS id h15-v6si310525ual.2.2018.06.14.02.58.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 02:58:25 -0700 (PDT) Received-SPF: pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::22c as permitted sender) client-ip=2607:f8b0:400e:c00::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ugCufGqQ; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::22c as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-pf0-x22c.google.com with SMTP id z24-v6so2976064pfe.7 for ; Thu, 14 Jun 2018 02:58:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=PrO4HnO9ucjodyj0CYzuBrl9OXQur1HLx1NTbkw3ZpY=; b=ugCufGqQbZLPTmoLvgvMLcUjJvf54N35KVgy7fWLfg4Cn3BYeHqr3jr+dvzplUYcJ1 bwK9fqggP/XSpw0+OcXNaugAPwupLv97ZRTasF+dIxFDUzK6UyeLZegwsw9hBmHVytAD MZ2/f4aGHm2t3pVZgx7iikIH+dLvdXHuIpq02iZGSrCe/hwOXC6EdFz1XO4xDNA8DyI0 JBlsU3Z1DPRGWDhtrboVTFgnOJ8ne5rcxuiXvwfmWocK3TInX0nYHUSwJIejrGd3mgNh UjNAWrcfHzBruhJMFiNRFQjwiwIWvMco+Jz621cGZbCXJYEN8IOGosl047oxDXKDnO2Q WO7A== X-Gm-Message-State: APt69E3CfZnUHzWaNuMnQ4KbiwxdkoJf0KSp8HC52QCRoGCIQ2xkuZIx 9euZyv11vn2j0gBBDOM1lcLVGF87p8dqFCnN/+PK4A== X-Received: by 2002:a65:66c6:: with SMTP id c6-v6mr1726020pgw.76.1528970304530; Thu, 14 Jun 2018 02:58:24 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:6686:0:0:0:0 with HTTP; Thu, 14 Jun 2018 02:58:23 -0700 (PDT) In-Reply-To: References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> From: Christian Sattler Date: Thu, 14 Jun 2018 11:58:23 +0200 Message-ID: Subject: Re: [HoTT] Quillen model structure To: Steve Awodey Cc: Michael Shulman , Thierry Coquand , Homotopy Theory Content-Type: multipart/alternative; boundary="000000000000dfae87056e972343" --000000000000dfae87056e972343 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 generate= d > 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) 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. > 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 maximal= no-trivial subobject, 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 living 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 a= ll n, G, and =E2=96=A1=E2=81=BF/G =E2=86=92 I. > 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 ca= n > 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 > type > >>>> theory with universes > >>>> (and conversely the fact that we have a fibrant universe is a crucia= l > >>>> 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 quotie= nt > >>>> 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 cubica= l > 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 this > is why > >>>> I post this note, > >>>> The point (2) is only a concrete description of Sattler=E2=80=99s ar= gument 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 the= ir > >>>> 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, sen= d > 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. > --000000000000dfae87056e972343 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On T= hu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wro= te:
but they are cofib= rantly generated:

- the cofibrations can be taken to be all monos (say), which are generated = 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=C2=A0 I^n +_= A (A x I) for all A >=E2=80=94> I^n cofibrant and there is some index= ing I^n =E2=80=94> I .=C2=A0 In any case, a small set of generating triv= ial cofibrations.

Those would be the ob= jects of a=C2=A0category of algebraic generators. For generators o= f the underlying weak factorization systems, one would take any cellular mo= del S of monomorphisms, here for example=C2=A0=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) a= nd =E2=88=82=E2=96=A1=E2=81=BF denotes the maximal no-trivial subobject, an= d for trivial cofibrations=C2=A0the corresponding generators=C2=A0= =CE=A3_I (S_{/I} hat(=C3=97)_{/I} d) with d : I =E2=86=92 I=C2=B2 the diago= nal (seen as living over I), i.e.=C2=A0=E2=96=A1=E2=81=BF/G +_{=E2=88=82=E2=96=A1=E2=81=BF/G} I=C2=A0=C3=97=C2=A0=E2=88= =82=E2=96=A1=E2=81=BF/G=C2=A0=E2=86=92 I=C2=A0= =C3=97=C2=A0=E2=96=A1=E2=81=BF/G for all n, G, and=C2=A0=E2=96=A1=E2=81=BF/G=C2=A0=E2=86=92 I.


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 <awo...@cmu.edu> wrote:
>> oh, interesting!
>> because it=E2=80=99s not defined over sSet, but is covered by it.<= br> >>
>>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>>>
>>> This is very interesting.=C2=A0 Does it mean that the (oo,1)-c= ategory
>>> 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
>>> <Thierry...@cse.gu.= se> wrote:
>>>> The attached note contains two connected results:
>>>>
>>>> (1) a concrete description of the trivial cofibration-fibr= ation
>>>> factorisation for cartesian
>>>> cubical sets
>>>>
>>>> It follows from this using results of section 2 of Christi= an Sattler=E2=80=99s
>>>> paper
>>>>
>>>> https://arxiv.org/pdf/1704.06911
>>>>
>>>> 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 type
>>>> theory with universes
>>>> (and conversely the fact that we have a fibrant universe i= s a crucial
>>>> component in the proof
>>>> that we have a model structure).
>>>>
>>>> I described essentially the same argument for factorisatio= n 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 ge= neral framework
>>>> in the paper of Andrew Swan
>>>>
>>>> https://arxiv.org/abs/1802.07588
>>>>
>>>>
>>>>
>>>> Since there is a canonical geometric realisation of cartes= ian cubical sets
>>>> (realising the formal
>>>> interval as the real unit interval [0,1]) a natural questi= on 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 equiv= alence.
>>>>
>>>> I believe that this result should be relevant even for peo= ple interested in
>>>> the more syntactic
>>>> aspects of type theory. It implies that=C2=A0 if we extend= cartesian cubical type
>>>> theory
>>>> with a type=C2=A0 which is a HIT built from a primitive sy= mmetric square q(x,y) =3D
>>>> q(y,z), we get a type
>>>> which should be contractible (at least its geometric reali= sation is) but 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 argument 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=C2=A0 =C2=A0= Cartesian cubes -> Dedekind
>>>> cubes (corresponding
>>>> to distributive lattices) is also not a Quillen equivalenc= e (for their
>>>> respective type theoretic model
>>>> structures). Hence, as noted by Steve, this implies that t= he model structure
>>>> obtained by transfer
>>>> and described at
>>>>
>>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf
>>>>
>>>> is not equivalent to the type-theoretic model structure. >>>>
>>>>=C2=A0 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 th= e Google Groups
>>>> "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving emails f= rom it, send an
>>>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>>>> For more options, visit https://groups.google.com= /d/optout.
>>>
>>> --
>>> You received this message because you are subscribed to the Go= ogle Groups "Homotopy Type Theory" group.
>>> To unsubscribe from this group and stop receiving emails from = it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
>>> For more options, visit https://groups.google.com/d/<= wbr>optout.
>>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--000000000000dfae87056e972343--