From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a19:48cd:: with SMTP id v196-v6mr158040lfa.34.1528990915461; Thu, 14 Jun 2018 08:41:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:9d47:: with SMTP id y7-v6ls888111ljj.0.gmail; Thu, 14 Jun 2018 08:41:54 -0700 (PDT) X-Received: by 2002:a2e:380a:: with SMTP id f10-v6mr167155lja.3.1528990914039; Thu, 14 Jun 2018 08:41:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528990913; cv=none; d=google.com; s=arc-20160816; b=aH+ND/3mo9z+tg6LTI0uZRVzIR87XaOpk+eJLQMFhjO6Bo/Kp/wysYJpInB5XVPVnZ ZSufKNT2+VchyZoPMUGPe+eanqqjHVv/HeifRZbarcpFiYc63/+qDOSrunEvAxPQNZ7S Y4bsuBllz1HXNZdyFTXiNWwKyIrQzubeIrSfwnZVG+tedjIogTO4LOEm41e8d9ZVdFFy 6XqttXJaUcZHK6M7OzDqPNPHfcvUI6Ri7C+exUVtCAVEwpWBrxYWq4a2syWM4mz5gnJQ WN7wwJ5vhyL98ZzHjneVr4UAM+Nne35NAOJEJ9zPNeGcaPt8Xd3SgIjjmsyCitpSZrjC J8iQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version:from :dkim-signature:arc-authentication-results; bh=J+C9cbrYrnUCJwxv4dwbyejzn8UHamglHSUsEQRvHUA=; b=WP0n9OZcTl6dNErrNHK/38fnaHhCWkDKr83x4jaK72gR8Ihwdz3s2KFld8zbM1tbf1 zAwQKczTuWBz6Iy0GPJPuO5/dMb36u0FZzEtMKh3EyV/wrwhLI3sq+QsI5AssA6RDmU9 LmeP4fuooNWYQsIdKnZPSc+MiNqK4uNOXhFJ4SHoEErZOgQmRE+xf9ex1r0TgVwys0nQ 4NxtXEIB17uzGSkntYMmLOVS/2G+88dTTTxP4dxK9kgeuKsn3fozxWfuDlV8sanXzdks /Aq+TWYO90IHg0t0sbhO6T1txkJS/eCDnoeLiX4w9fWwKnJqb8AtwOKDN/rWoG0Fu1Hf 62Ww== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=Mzkrzif6; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22f 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-x22f.google.com (mail-wm0-x22f.google.com. [2a00:1450:400c:c09::22f]) by gmr-mx.google.com with ESMTPS id y2-v6si181652lfi.5.2018.06.14.08.41.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 08:41:53 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22f as permitted sender) client-ip=2a00:1450:400c:c09::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=Mzkrzif6; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22f 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-x22f.google.com with SMTP id 69-v6so12848105wmf.3 for ; Thu, 14 Jun 2018 08:41:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=from:mime-version:subject:date:references:to:in-reply-to:message-id; bh=J+C9cbrYrnUCJwxv4dwbyejzn8UHamglHSUsEQRvHUA=; b=Mzkrzif6GOr5CQufF0kniP5HP32BlFN28r1l8ae0D3EvBOW3nvNL072Hu1gPDvYUed Ed6r7krDEgOYiiEdc0pPu8wFgg2hAPhv0hG9BvqVO07TURqW1ffeyiFy/JKDUB271DT8 DrdohR0BHzA1VjZIn2DVam2KbJXhOvlaYAjkWXl1/P/VacC92p/MYY1JnO/Ak+5XdMfs DFaIc16c4StQnnFzLAqMONo1vbn/MD2rxJsYqCMKEAKFSEvNApwiAF0qBZ5f0bCwpq++ gydntESDadWX32lmNYCDnJb4An5zysW3cDAnnLU+SACBnnLyL8fN3J98b4lWYdzrg2np aiNQ== X-Gm-Message-State: APt69E1cpkIFS9qx5kUNlhaZREVODHA/ZATAU3q67tGqInJepbNJ//AS oyGU3LowsUOf/ws0UvcgLAUE7/c6N4M= X-Received: by 2002:a1c:9c0b:: with SMTP id f11-v6mr2265032wme.148.1528990913385; Thu, 14 Jun 2018 08:41:53 -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 q17-v6sm6947797wrr.7.2018.06.14.08.41.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 08:41:52 -0700 (PDT) From: Steve Awodey Content-Type: multipart/alternative; boundary="Apple-Mail=_C691FF0B-E4D2-425F-8838-AC20AB03D7AB" Mime-Version: 1.0 (Mac OS X Mail 11.3 \(3445.6.18\)) Subject: Re: [HoTT] Quillen model structure Date: Thu, 14 Jun 2018 17:42:13 +0200 References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> To: Homotopy Theory In-Reply-To: Message-Id: X-Mailer: Apple Mail (2.3445.6.18) --Apple-Mail=_C691FF0B-E4D2-425F-8838-AC20AB03D7AB Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 1 correction: > 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 =20 >=20 > m xo d : I^n +_A (A x I) >=E2=80=94> B x I should be: =09m xo d : B +_A (A x I) >=E2=80=94> B x I Steve >=20 > is formed over I as previously described. >=20 > yes? >=20 > Yes, that's correct. > =20 >=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: >>> 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 >>>=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 g= enerators 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 subo= bject, >>=20 >> this determines the same class of cofibrations as simply taking *all* su= bobjects of representables, which is already a set. There is no reason 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 = 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. >>=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 composi= tion 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 Sattl= er=E2=80=99s >>> >>>> paper >>> >>>>=20 >>> >>>> https://arxiv.org/pdf/1704.06911 >>> >>>>=20 >>> >>>> 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 is a cruc= ial >>> >>>> component in the proof >>> >>>> that we have a model structure). >>> >>>>=20 >>> >>>> I described essentially the same argument for factorisation in a m= essage >>> >>>> to this list last year >>> >>>> July 6, 2017 (for another notion of cubical sets however): no quot= ient >>> >>>> operation is involved >>> >>>> in contrast with the "small object argument=E2=80=9D. >>> >>>> This kind of factorisation has been described in a more general fr= amework >>> >>>> 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 cubi= cal 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 inte= rested in >>> >>>> the more syntactic >>> >>>> aspects of type theory. It implies that if we extend cartesian cu= bical type >>> >>>> theory >>> >>>> with a type which is a HIT built from a primitive symmetric squar= e q(x,y) =3D >>> >>>> q(y,z), we get a type >>> >>>> which should be contractible (at least its geometric realisation i= s) but we >>> >>>> cannot show this in >>> >>>> cartesian cubical type theory. >>> >>>>=20 >>> >>>> It is thus important to understand better what is going on, and th= is 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. >>> >>>>=20 >>> >>>> Note that this implies that the canonical map Cartesian cubes ->= Dedekind >>> >>>> cubes (corresponding >>> >>>> to distributive lattices) is also not a Quillen equivalence (for t= heir >>> >>>> 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 dis= cussions >>> >>>> 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, s= end 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 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 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 --Apple-Mail=_C691FF0B-E4D2-425F-8838-AC20AB03D7AB Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
1 correction:

gen= erators 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 som= e 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
=

should be:
=09m xo d : B +_A (A x I) >=E2=80= =94> B x I

Ste= ve

is formed over I as previously described.=

yes?
=

Yes, that= 's correct.
 

Steve


On Jun 14, 2018, at 12:27 PM, Steve Awodey <awo...@cmu.edu> wrote:=



On Jun 14, 2018, at 11:58 AM, Christian S= attler <sattler....@gmail.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 .&= nbsp; 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=09=09v
=09I^n =E2=80=94=E2=80=94>  I^n x I
<= span class=3D"m_-7722557941428220398Apple-tab-span" style=3D"white-space:pr= e-wrap">=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 me= ntioned above.

St= eve





=


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+unsubscribe@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+unsubscribe@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+unsubscribe@googlegrou= ps.com.
For more options, visit https://groups.google.com/d/op= tout.

<= br class=3D"m_-7722557941428220398webkit-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 HomotopyTypeTheory+unsub...@googlegroups.c= om.
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 HomotopyTypeTheory+unsub...@googlegroups.c= om.
For more options, visit https://groups.google.com/d/optout= .


--Apple-Mail=_C691FF0B-E4D2-425F-8838-AC20AB03D7AB--