From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:d0ca:: with SMTP id u10-v6mr2384268edo.4.1528972073697; Thu, 14 Jun 2018 03:27:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:f317:: with SMTP id p23-v6ls2998340edm.3.gmail; Thu, 14 Jun 2018 03:27:52 -0700 (PDT) X-Received: by 2002:aa7:d486:: with SMTP id b6-v6mr2361625edr.7.1528972072500; Thu, 14 Jun 2018 03:27:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528972072; cv=none; d=google.com; s=arc-20160816; b=sHbLF0i52/J9tcG9ZPIYXO0kH2zD+pTMiH1Lg8+kxN0to0cy8xXWqwMwsTNSN9/Itg zPhTngsSBk3bx7ip80LdsV2iczYcdZi+7YfBQw4tve3vD/chBI3ujnVosu2e+DOLkRoP /SiNHrJuTdX3VdraMvGVe/a8R8vS5Snfd/tmrqWcCSLahS6QcHi5goPFnYWluZQKkeqp iXZkruYw6mizoaEv36K/BGKXO0sSyHY2nLIwhwhRn0TZ5ys2Nw/3AB9vFvTCg5+9e+pD 4G2XwZgJuLSzbsxl9wLtrEdNDXPPs1jMNaA0PaqF5iYgCu097AHkmcpz0PZ2KS9nTV++ Q7Hw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature:arc-authentication-results; bh=OiJZIqFJ/srWHJ9AWEFnA/cpQJqN4spjrBMQbDi6I3U=; b=xWW3kQDQ1EDFEVwy8pqd1WSZM4MBW+kX7v2ckTANzQpnKeIZAjPO0HpyEFsyH3CctS 9iphmYm1INDsXqdIyoH2NxW1txX+G+/AjR/DFSRzhtyykDg3oERZ6/h1ciyjTh8BCXOE RpNdPsrkAfH16YYzjtAKal3V2fz8rViedtr4jczIiD3rnCJXJW2CgCMcV5hqN3XhhUkh WWw5DK+ZIsA/2hefISARDzceE5cLsTlxV5SfkM5wZR0mf3JJqvK4xqMPQ/9BrAAFVggR tvR1111b46HvruPDbeIOeoP0pnDCq4YjI2HsIs83265YsMEU69HhaQqI6ZD6iP5UTm1a cDUQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=pA9hYeTl; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::229 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-x229.google.com (mail-wr0-x229.google.com. [2a00:1450:400c:c0c::229]) by gmr-mx.google.com with ESMTPS id x7-v6si219996edh.5.2018.06.14.03.27.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 03:27:52 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::229 as permitted sender) client-ip=2a00:1450:400c:c0c::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=pA9hYeTl; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::229 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-x229.google.com with SMTP id l10-v6so5853061wrn.2 for ; Thu, 14 Jun 2018 03:27:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references; bh=OiJZIqFJ/srWHJ9AWEFnA/cpQJqN4spjrBMQbDi6I3U=; b=pA9hYeTl1T7E/t1uZ73HCHO16mU+BSnxm58VlgkX95aodkn3aNvk7UwcubKd33IS3W NlftqfRlaNMmwQRHyzvqzxSk5ueHupjzhbvdJxCatRO0QAWuiqTMy7Erz3wLFnOXRzRt fuN4jHXzOH2kAaPBDNsGtkUFGI3ZQ3AsIJqaMCMBJt6PLTPkIJNvwn2QsLGx9E0l0Ah8 9eb9OerRQnctYaOSod+RbuWyFaLAb3BPLj5ETnZXvJdmeI3aLElA2lMaBBvNOP6D/Eh5 ezbfZwM85RnOF+r1bL0zZ5DJRuTKSJNzKgX8SOwOIyY8AxOPCWXwn0DO9TMFhzYbIcFJ WTyQ== X-Gm-Message-State: APt69E1DqHx9H3SGuUBiFJl+WmXP1dr/WbwEgLDhBAusgajCM5NsCu3z EDJnVIa6UqKCVPHEPWQ0WbNsrFioxP8= X-Received: by 2002:adf:a6ca:: with SMTP id t68-v6mr1591403wrc.215.1528972072209; Thu, 14 Jun 2018 03:27:52 -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 v31-v6sm11442093wrc.80.2018.06.14.03.27.51 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 03:27:51 -0700 (PDT) From: Steve Awodey Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_9B759120-A039-435D-BF67-2A8EFA3B33B7" Mime-Version: 1.0 (Mac OS X Mail 11.3 \(3445.6.18\)) Subject: Re: [HoTT] Quillen model structure Date: Thu, 14 Jun 2018 12:27:50 +0200 In-Reply-To: Cc: Michael Shulman , Thierry Coquand , Homotopy Theory To: Christian Sattler References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> X-Mailer: Apple Mail (2.3445.6.18) --Apple-Mail=_9B759120-A039-435D-BF67-2A8EFA3B33B7 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > On Jun 14, 2018, at 11:58 AM, Christian Sattler w= rote: >=20 > On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey > wrote: > but they are cofibrantly generated: >=20 > - the cofibrations can be taken to be all monos (say), which are generate= d by subobjects of cubes as usual, and=20 >=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 > Those would be the objects of a category of algebraic generators. For gen= erators of the underlying weak factorization systems, one would take any ce= llular 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 subobje= ct, this determines the same class of cofibrations as simply taking *all* subob= jects 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 compositio= n with j. Over I we also have the generic point d : I =E2=80=94> I x I , s= o 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 indexing over I to end up with the descr= iption I already gave, namely: U =3D I^n +_A (A x I) 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,=20 there is a commutative square: =09=09g =09A =E2=80=94=E2=80=94 >=09A x I =09|=09=09| m=09|=09=09|=09m x I =09|=09=09| =09v=09=09v =09I^n =E2=80=94=E2=80=94> I^n x I =09|=09h j=09| =09v =09I put the usual pushout U =3D I^n +_A (A x I) inside it,=20 and the comprison map U =E2=80=94> I^n x I is the m xo d mentioned above. Steve >=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 ca= n call > >>>> =E2=80=9Ctype-theoretic=E2=80=9D > >>>> since it is built on ideas coming from type theory), which can be do= ne 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). > >>>>=20 > >>>> I described essentially the same argument for factorisation in a mes= sage > >>>> 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 fram= ework > >>>> 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 cubica= l sets > >>>> (realising the formal > >>>> interval as the real unit interval [0,1]) a natural question is if t= his 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 intere= sted in > >>>> the more syntactic > >>>> aspects of type theory. It implies that if we extend cartesian cubi= cal 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 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 s= ets > >>>> however), which should bring > >>>> further lights on this question. > >>>>=20 > >>>> Note that this implies that the canonical map Cartesian cubes -> D= edekind > >>>> 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 s= tructure > >>>> 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 discu= ssions > >>>> about this last week in Bonn. > >>>>=20 > >>>> -- > >>>> You received this message because you are subscribed to the Google G= roups > >>>> "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 > >>> -- > >>> You received this message because you are subscribed to the Google Gr= oups "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 . > >>=20 >=20 > --=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 >=20 > --=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 . --Apple-Mail=_9B759120-A039-435D-BF67-2A8EFA3B33B7 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8

On Jun 14, 20= 18, at 11:58 AM, Christian Sattler <sattler....@gmail.com> wrote:

On Thu, Jun 14, 2018 at 11:28= AM, Steve Awodey <awo...@cmu.edu> wrote:=
but they a= re cofibrantly 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  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 .  In any case, a small set of generating triv= ial cofibrations.

Those would be the objects of a ca= tegory of algebraic generators. For generators of the underlying wea= k factorization systems, one would take any cellular model S of monomorphis= ms, 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,

this determines the same c= lass of cofibrations as simply taking *all* subobjects of representables, w= hich is already a set.  There is no reason to act by Aut(n), etc., her= e.

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 all n, G, and =E2=96=A1=E2= =81=BF/G =E2=86=92 I.<= /span>

sorry, I can=E2=80=99t read your notation.

=
the generating trivial cofibrations I stated are the following:<= /div>

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 c= an 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-o= ut product of d and m over I , say m xo d : U >=E2=80=94> I^n x I . &= nbsp;Then we forget the indexing over I to end up with the description I al= ready gave, namely:

U =3D  I^n +_A (A x I)
where the indexing j is built into th= e 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:

=09=09g
=09A =E2=80=94=E2=80=94 >=09A x I
=09|=09=09|
m=09|=09=09|=09m x I
=09|=09=09|
=09v=09=09v
=09I^n =E2=80=94=E2=80=94&g= t;  I^n x I
=09|=09h
j=09|
=09v
=09I

put the usua= l pushout U =3D I^n +_A (A x I) inside it, 
and the compriso= n 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 <awo...@cmu.edu> wrote:
>> oh, interesting!
>> because it=E2=80=99s not defined over sSet, but is covered by it.<= br class=3D""> >>
>>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> wrote: >>>
>>> This is very interesting.  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  if we extend= cartesian cubical type
>>>> theory
>>>> with a type  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   = 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/h= ottmuri/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 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.goo= gle.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 e= mail to = HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

<= br class=3D"webkit-block-placeholder">
--
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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_9B759120-A039-435D-BF67-2A8EFA3B33B7--