From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:b496:: with SMTP id y22-v6mr549603plr.28.1528987953533; Thu, 14 Jun 2018 07:52:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:504b:: with SMTP id k11-v6ls1667098pgo.27.gmail; Thu, 14 Jun 2018 07:52:32 -0700 (PDT) X-Received: by 2002:a63:7319:: with SMTP id o25-v6mr480792pgc.154.1528987952437; Thu, 14 Jun 2018 07:52:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528987952; cv=none; d=google.com; s=arc-20160816; b=VVdI04sml7w0+qjSATVUAksL051Vj8ViJAqz9G+URC41YGd7gDq01YKiG/7v2mBaal 23aXphkI60EKx+lam+S+ACxv1stxGFZRhDXY7gkhEnnMAPkSOAlJIE0cflora2GhRRyU 3lt5PRsKbhxPZPRGH86eMkPCSg0gfvJjQsKbVALXQm9jH7xm38tnI+lTPppheLbcaU2x OlPr0Mm+KriEo5wB0rpeeGCbrYaap1wo4uy6YJTQyE0/GZXh2dJ/9unlHF0TIgGK8XDt fNJgeh0XPeqqIIKgb79oxZ+B+OAVcgc75L1lCLYlAuYId5VJzWcs48LggtIHrmA5nH6S amXg== 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=o4vqJbU/N2BApP4LFVo34ZVKXoekt/YtxifUm1+oAls=; b=xa4HkP7ABDRsTRTUU2QamWcjDQGebYnMRdOpiOLIh9S7RGNHTyEr/NAAYtKcz9esoE +Kz1AUljuQyGc4WdZHubO2ncGqg/mVBFi3tStS1FG0/NSJXmQftkxYEJV98xiF6mY3t9 bjplqAv4c4kn9wahtbD4VyF4gGnuYNxXwYamPoDxNwXFmRSsr9GNDym1nHJw3818HnaS TR5bj6oWPqUrNfBncPMS7AUXdsDCwyS5+FVsmWbsF6Cxw2XcxWTGnW8oEq3o+VeFZw1N NrecCUYC4SD98e45sGqfVvEbwKRTGwTx40quTOFHDjZ1moWxubGrXLYpd8z8/QQO1fou 3DQQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=P721B3yF; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::236 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-x236.google.com (mail-pf0-x236.google.com. [2607:f8b0:400e:c00::236]) by gmr-mx.google.com with ESMTPS id e6-v6si302272pfn.1.2018.06.14.07.52.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 07:52:32 -0700 (PDT) Received-SPF: pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::236 as permitted sender) client-ip=2607:f8b0:400e:c00::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=P721B3yF; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::236 as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-pf0-x236.google.com with SMTP id w7-v6so3359992pfn.9 for ; Thu, 14 Jun 2018 07:52:32 -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=o4vqJbU/N2BApP4LFVo34ZVKXoekt/YtxifUm1+oAls=; b=P721B3yFr00MopNNjFFShsF+9KKAKqU4kcD0Vwh3OtnQYThr0KvrAkSIpMGaiGjUTH 4dj7nRGxBWoTGvhkX8OrTXXsi9pP9xGFOVNFL0jXWexGM/VO5b8nP9VVEMdPl4tyUDmv 2t6P/GCTPzle+xadsM/ENs4uDBfv3nYUEAC2Y071EHgCR84Gj+JAAonvo9v/g4cp3qkN vX54i5zDOTrQr8uCFnVZ2+nSNEbRU5N+DsNSbjjnzLV9ty5NHxAJro432Oa3kNTA02i7 i90MiyZi3xzcWFg0rJeDImZn8hNM2oYD2BzjgP8YWZQFNl6/3rD6X/wrKQekx5e0pmY8 dwRQ== X-Gm-Message-State: APt69E3hbKAJjpTnlhFd7XGfgxrj4zzPnNpw9qIgz8xPxCimfpUUQTKF 7/oivvPe8hxdeHVZpw/c3e0R6/JYRVud9hnU7d4= X-Received: by 2002:a62:f615:: with SMTP id x21-v6mr9796617pfh.43.1528987952135; Thu, 14 Jun 2018 07:52:32 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:6686:0:0:0:0 with HTTP; Thu, 14 Jun 2018 07:52:31 -0700 (PDT) In-Reply-To: References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> From: Christian Sattler Date: Thu, 14 Jun 2018 16:52:31 +0200 Message-ID: Subject: Re: [HoTT] Quillen model structure To: Steve Awodey Cc: Michael Shulman , Thierry Coquand , Homotopy Theory Content-Type: multipart/alternative; boundary="000000000000c0c1ed056e9b3fb5" --000000000000c0c1ed056e9b3fb5 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Jun 14, 2018 at 3:44 PM, 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 > arrows), and then take the underlying (non-algebraic) wfs by closing unde= r > 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 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? > Yes, that's correct. > > Steve > > > On Jun 14, 2018, at 12:27 PM, Steve Awodey wrote: > > > > On Jun 14, 2018, at 11:58 AM, Christian Sattler < > sattler....@gmail.com> 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 >> 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 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 > indexing 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 >> 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 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 >> cubical 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, >> 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 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. > > > --000000000000c0c1ed056e9b3fb5 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On T= hu, Jun 14, 2018 at 3:44 PM, Steve Awodey <awo...@cmu.edu> wrot= e:
Ok, I think I see what you are saying:

<= /div>
we can generate an *algebraic wfs* using the generators I gave pr= eviously (regarded as a *category*, with pullback squares of monos, etc., a= s arrows), and then take the underlying (non-algebraic) wfs by closing unde= r retracts, as usual, and the result is then cofibrantly generated by the *= set* of maps you are describing, which consists of quotients of the origina= l ones.

generators aside, the cofibrations are all= the monos, and the fibrations have the RLP w/resp. to all push-out product= s m xo d : U >=E2=80=94> B x I, where m : A >=E2=80=94> B is an= y 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 ov= er I, and the pushout-product =C2=A0

m xo d : I^n = +_A (A x I) =C2=A0>=E2=80=94> =C2=A0B x I

is= formed over I as previously described.

yes?
=

Yes, that's correct.
= =C2=A0

Steve


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



On Jun = 14, 2018, 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 are cofibrantly gener= ated:

- 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,

this determines the= same class of cofibrations as simply taking *all* subobjects of representa= bles, which is already a set.=C2=A0 There is no reason to act by Aut(n), et= c., here.

and for trivial c= ofibrations=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 diagonal (seen as livi= ng 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=86=92 I.

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

the gene= rating 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.=C2=A0 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 .=C2=A0 Then we forget the indexi= ng over I to end up with the description I already gave, namely:
=
U =3D =C2=A0I^n +_A (A x I)

where the indexing j is b= uilt into the pushout over A. =C2=A0

A more direct= description is this:=C2=A0

let h : I^n =E2=80=94&= gt; I^n x I be the graph of j,
let g : A =E2=80=94> A x I be t= he graph of j.m,=C2=A0
there is a commutative square:
<= br>
=09=09g
=09A =E2=80= =94=E2=80=94 >=09A x I
=09|=09=09|
m=09|=09=09|=09m=C2=A0x I
=09|=09=09|
=09v=09=09v
=09I^n =E2=80=94=E2=80=94> =C2=A0I^n x = I
=09|=09h
j= =09|
=09v
=09I

put the usual pushout U =3D I^n +_A (A x I) inside = it,=C2=A0
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 <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> wr= ote:
>>>
>>> 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+unsubscribe@googlegroups.c= om.
>>>> 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.google.com/d/o= ptout.
>>

--
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--000000000000c0c1ed056e9b3fb5--