From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:d0ca:: with SMTP id u10-v6mr2545364edo.4.1528983901005; Thu, 14 Jun 2018 06:45:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:c247:: with SMTP id y7-v6ls3115358edo.2.gmail; Thu, 14 Jun 2018 06:44:59 -0700 (PDT) X-Received: by 2002:aa7:c6d7:: with SMTP id b23-v6mr2542759eds.0.1528983899879; Thu, 14 Jun 2018 06:44:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528983899; cv=none; d=google.com; s=arc-20160816; b=K02gI0AYGmLyE9/LyMYuKGBf2UJ6XF5j3P4Tbz/qsceOgkXmeyLhFhuYUp/4oQkCju GCxYhDP2SdKEO/0pgJ+Be1A2q+mgH+pZRGSwEebREyM/vnvhe4J/4FeKxWemJyKynDqV giPKvvXhXKMtwC7d0HsJnA4+Zsn3nJYRrAPMZTmtzxFEDIp1SAjn5C8cpXxJx4jwkJU3 dC22uN70L9+9Dojp57VCh6AmvJa8r4r3ZcrFarpGZl+GDtDGdMjdkdWIu8PJ+pAeiU9r yjPtcc3RXWpCqlG2Uzk1HE0OQQ8up2xAxKlaTkbMUKD0To5yQn/U1uABLcaAZBZfHgfu FFJQ== 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=dcmmJYQMOOf5th2Zi0uVBPShyrDn1xH+isxrlq6gWpQ=; b=S563CKnAKqhobfL1XUgp0cMkNeM1vXpj448x1SdW3WcLE72Be/tYWdX83tXIxxDvko 8BNWio00rSnqdctUm895JdKxLaPWELYhr5swFOd4Jkdp6oEdyMp0zJxOxewKdw0CV0tj ixOq0ClcBzWnbKRXlYqVq1NL2Q9lh1pYVTdhN5wQpIPlOW7A2fNYgPlE1PIrqLxXy2lN u4HJRyDWgYI+cPIzrhPd49HPe8JjkXgtFYTZlmwAVPXXIdnVnljUPePEFn1JmhNcDYPS M/dTEWry2jvAREjuHCj2jSV9YWd8rxl0ePZVP6Okbgs+cIAyiRn38jdonBXNSziYlfob tSqQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=WBVuc5jN; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::242 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-x242.google.com (mail-wm0-x242.google.com. [2a00:1450:400c:c09::242]) by gmr-mx.google.com with ESMTPS id e5-v6si215115edi.4.2018.06.14.06.44.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 06:44:59 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::242 as permitted sender) client-ip=2a00:1450:400c:c09::242; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=WBVuc5jN; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::242 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-x242.google.com with SMTP id p11-v6so12083776wmc.4 for ; Thu, 14 Jun 2018 06:44:59 -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=dcmmJYQMOOf5th2Zi0uVBPShyrDn1xH+isxrlq6gWpQ=; b=WBVuc5jNso/Nf5rY/h+WyN0rRJdhFmFGCun6xppuHmL2+qWx/tB6Gn1fSfvsRFbuZv +VVn0qkz+dcOPd0ke18xYgQaT0S47xax2oLIFgKPi932kxBhVE2sKBvk9BDyi0h3xhLw O19G7pw4A0+0MmXG5LBv4O162aAcddX0ACgfjv1giEQz6yam69NzceTjrLJUrftrMSx8 mPrilURfKZOGx/uPI77Aah70dr8DLRWGaavT+3kVW3Ihgx8KtSCLdSS76tZgjLMpQdJ7 r9gt/NyB/1RqgJBjn8/7WsSFQ15iazM5TQSKzVAij265vE4vsWwcFt2ZozppA2f4/EOV NXYw== X-Gm-Message-State: APt69E1DOx7H3U1V+/UTCt4eFtj2KSO3VPINhMUEL77STEjCT6enapbI fecWCHdk/3jZUQAokd6CnZsaGg== X-Received: by 2002:a1c:256:: with SMTP id 83-v6mr2104718wmc.41.1528983899508; Thu, 14 Jun 2018 06:44:59 -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 j21-v6sm3955030wme.36.2018.06.14.06.44.58 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 06:44:58 -0700 (PDT) From: Steve Awodey Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_0540660A-8E56-4B0C-9B62-59BE2AB6B000" Mime-Version: 1.0 (Mac OS X Mail 11.3 \(3445.6.18\)) Subject: Re: [HoTT] Quillen model structure Date: Thu, 14 Jun 2018 15:44:57 +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=_0540660A-8E56-4B0C-9B62-59BE2AB6B000 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 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 arrows),= and then take the underlying (non-algebraic) wfs by closing under retracts= , 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 ha= ve the RLP w/resp. to all push-out products m xo d : U >=E2=80=94> B x I, w= here m : A >=E2=80=94> B is any mono, j : B =E2=80=94> I is some indexing m= aking 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 =20 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: >=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: >> but they are cofibrantly generated: >>=20 >> - the cofibrations can be taken to be all monos (say), which are generat= ed 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 ge= nerators of the underlying weak factorization systems, one would take any c= ellular 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, >=20 > this determines the same class of cofibrations as simply taking *all* sub= objects of representables, which is already a set. There is no reason to a= ct 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 > 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 composit= ion 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 indexing over I to end up with the de= scription 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 >=20 > A more direct description is this:=20 >=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: >=20 > =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 >=20 > 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. >=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 Sattle= r=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 d= one 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 me= ssage >> >>>> to this list last year >> >>>> July 6, 2017 (for another notion of cubical sets however): no quoti= ent >> >>>> operation is involved >> >>>> in contrast with the "small object argument=E2=80=9D. >> >>>> This kind of factorisation has been described in a more general fra= mework >> >>>> 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 inter= ested in >> >>>> the more syntactic >> >>>> aspects of type theory. It implies that if we extend cartesian cub= ical 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 th= eir >> >>>> 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 disc= ussions >> >>>> 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, s= end 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 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 >>=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 > --=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=_0540660A-8E56-4B0C-9B62-59BE2AB6B000 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Ok, I think I see what you= are saying:

we can gen= erate an *algebraic wfs* using the generators I gave previously (regarded a= s a *category*, with pullback squares of monos, etc., as arrows), and then = take the underlying (non-algebraic) wfs by closing under retracts, as usual= , and the result is then cofibrantly generated by the *set* of maps you are= describing, which consists of quotients of the original ones.

generators aside, the cofibra= tions are all the monos, and the fibrations have the RLP w/resp. to all pus= h-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 generi= c 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 <awo...@cmu.edu> wrote:



On Jun 14, 2018, at 11:58 AM, Christian Sattl= er <sattler....@gmai= l.com> wrote:

On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote:
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

- 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 class of cofibrations as simply taking *all* subobjects of repres= entables, which is already a set.  There is no reason to act by Aut(n)= , etc., here.

and for tri= vial 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 a= s 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&nb= sp;=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 not= ation.

the genera= ting trivial cofibrations I stated are the following:
=
take any =E2=80=9Cindexing=E2=80=9D ma= p 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 als= o 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 indexing over I to end up with the description I a= lready gave, namely:

U =3D  I^n +_= A (A x I)

where the inde= xing 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 commu= tative 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<= span class=3D"Apple-tab-span" style=3D"white-space:pre">=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, = ;
and the comprison map U =E2=80=94> I^n x I is the= m xo d mentioned above.

Steve





<= font color=3D"#888888" class=3D"">
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.


--
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=_0540660A-8E56-4B0C-9B62-59BE2AB6B000--