Quillen model structure

Quillen model structure

[Thierry Coquand]

[-- Attachment #1.1: Type: text/plain, Size: 2768 bytes --]

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’s paper

 https://arxiv.org/pdf/1704.06911

that we have a model structure on cartesian cubical sets (that we can call “type-theoretic”
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 crucial 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”.
 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) = 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’s 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 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.


[-- Attachment #1.2: Type: text/html, Size: 4870 bytes --]

[-- Attachment #2: fact1.pdf --]
[-- Type: application/pdf, Size: 168794 bytes --]

Re: [HoTT] Quillen model structure

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 3936 bytes --]


Hello

 Sorry for this problem. I should have used the following link

 https://ncatlab.org/homotopytypetheory/files/awodeyMURI18.pdf

 Best regards,
 Thierry


On 11 Jun 2018, at 10:28, Hiroyuki Miyoshi <h...@cc.kyoto-su.ac.jp<mailto:h...@cc.kyoto-su.ac.jp>> wrote:

Hi, Thierry,

Your note is very interesting for me!
Unfortunately, the Awodey's filie you mentioned in your message
seems to be (still?) private and I cannot read it:
https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf
If you (or Steve?) can change the status of the file, please make it public.
Thanks in advance.

Hiroyuki Miyoshi,
Dept of Mathematics, Kyoto Sangyo University, Kyoto, Japan
h...@cc.kyoto-su.ac.jp<mailto:h...@cc.kyoto-su.ac.jp>


2018年6月10日(日) 22:31 Thierry Coquand <Thierry...@cse.gu.se<mailto:Thierry...@cse.gu.se>>:

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’s paper

https://arxiv.org/pdf/1704.06911

that we have a model structure on cartesian cubical sets (that we can call “type-theoretic”
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 crucial 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”.
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) = 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’s 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 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<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Type: text/html, Size: 16205 bytes --]

Re: [HoTT] Quillen model structure

[Michael Shulman]

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
<Thierry...@cse.gu.se> 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’s
> paper
>
>  https://arxiv.org/pdf/1704.06911
>
> that we have a model structure on cartesian cubical sets (that we can call
> “type-theoretic”
> 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 crucial
> 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”.
>  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) =
> 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’s 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 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.

Re: [HoTT] Quillen model structure

[Steve Awodey]

oh, interesting!
because it’s not defined over sSet, but is covered by it.

> 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)-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
> <Thierry...@cse.gu.se> 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’s
>> paper
>> 
>> https://arxiv.org/pdf/1704.06911
>> 
>> that we have a model structure on cartesian cubical sets (that we can call
>> “type-theoretic”
>> 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 crucial
>> 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”.
>> 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) =
>> 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’s 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 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.

Re: [HoTT] Quillen model structure

[Michael Shulman]

In the 1-categorical case, I believe that every locally small
(co)complete elementary 1-topos is defined over Set: its global
sections functor has a left adjoint by cocompleteness, and the left
adjoint is left exact by the Giraud exactness properties (which hold
for any (co)complete elementary 1-topos).  Such a topos can only fail
to be Grothendieck by lacking a small generating set.

In the oo-case, certainly cartesian cubical sets present a locally
small (oo,1)-category (any model category does, at least assuming its
locally small as a 1-category), so it seems to me there are three
possibilities:

1. Although they are presumably an "elementary (oo,1)-topos" in the
finitary sense that provides semantics for HoTT with HITs and
univalent universes, they might fail to satisfy some of the oo-Giraud
exactness properties.  Presumably they are locally cartesian closed
and coproducts are disjoint, so it would have to be that not all
groupoids are effective.

2. They might lack a small generating set, i.e. the (oo,1)-category
might not be locally presentable.  Every combinatorial model category
(i.e. cofibrantly generated model structure on a locally presentable
1-category) presents a locally presentable (oo,1)-category, and the
1-category of cartesian cubical sets is certainly locally presentable,
but I suppose it's not obvious whether these weak factorization
systems are cofibrantly generated.

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’s not defined over sSet, but is covered by it.
>
>> 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)-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
>> <Thierry...@cse.gu.se> 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’s
>>> paper
>>>
>>> https://arxiv.org/pdf/1704.06911
>>>
>>> that we have a model structure on cartesian cubical sets (that we can call
>>> “type-theoretic”
>>> 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 crucial
>>> 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”.
>>> 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) =
>>> 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’s 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 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.
>

Re: [HoTT] Quillen model structure

[Steve Awodey]

> On Jun 14, 2018, at 12:00 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> In the 1-categorical case, I believe that every locally small
> (co)complete elementary 1-topos is defined over Set: its global
> sections functor has a left adjoint by cocompleteness, and the left
> adjoint is left exact by the Giraud exactness properties (which hold
> for any (co)complete elementary 1-topos).  Such a topos can only fail
> to be Grothendieck by lacking a small generating set.

yes, that’s correct.

> 
> In the oo-case, certainly cartesian cubical sets present a locally
> small (oo,1)-category (any model category does, at least assuming its
> locally small as a 1-category), so it seems to me there are three
> possibilities:
> 
> 1. Although they are presumably an "elementary (oo,1)-topos" in the
> finitary sense that provides semantics for HoTT with HITs and
> univalent universes, they might fail to satisfy some of the oo-Giraud
> exactness properties.  Presumably they are locally cartesian closed
> and coproducts are disjoint, so it would have to be that not all
> groupoids are effective.

that’s possible, I suppose …

> 
> 2. They might lack a small generating set, i.e. the (oo,1)-category
> might not be locally presentable.  Every combinatorial model category
> (i.e. cofibrantly generated model structure on a locally presentable
> 1-category) presents a locally presentable (oo,1)-category, and the
> 1-category of cartesian cubical sets is certainly locally presentable,
> but I suppose it's not obvious whether these weak factorization
> systems are cofibrantly generated.

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 >—> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I .  In any case, a small set of generating trivial cofibrations.


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’s not defined over sSet, but is covered by it.
>> 
>>> 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)-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
>>> <Thierry...@cse.gu.se> 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’s
>>>> paper
>>>> 
>>>> https://arxiv.org/pdf/1704.06911
>>>> 
>>>> that we have a model structure on cartesian cubical sets (that we can call
>>>> “type-theoretic”
>>>> 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 crucial
>>>> 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”.
>>>> 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) =
>>>> 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’s 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 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.
>> 

Re: [HoTT] Quillen model structure

[Bas Spitters]

There has been some work by Nicolas Tabareau's group to try and prove
the exactness properties.
E.g.
https://homotopytypetheory.org/2016/01/08/colimits-in-hott/
https://jfr.unibo.it/article/download/6232/6389
and perhaps even later work.

It would be interesting if the Cartesian cubes would provide a
counterexample to this approach, and show that a 2-level type theory
is really needed.

On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote:
>
>
>> On Jun 14, 2018, at 12:00 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>>
>> In the 1-categorical case, I believe that every locally small
>> (co)complete elementary 1-topos is defined over Set: its global
>> sections functor has a left adjoint by cocompleteness, and the left
>> adjoint is left exact by the Giraud exactness properties (which hold
>> for any (co)complete elementary 1-topos).  Such a topos can only fail
>> to be Grothendieck by lacking a small generating set.
>
> yes, that’s correct.
>
>>
>> In the oo-case, certainly cartesian cubical sets present a locally
>> small (oo,1)-category (any model category does, at least assuming its
>> locally small as a 1-category), so it seems to me there are three
>> possibilities:
>>
>> 1. Although they are presumably an "elementary (oo,1)-topos" in the
>> finitary sense that provides semantics for HoTT with HITs and
>> univalent universes, they might fail to satisfy some of the oo-Giraud
>> exactness properties.  Presumably they are locally cartesian closed
>> and coproducts are disjoint, so it would have to be that not all
>> groupoids are effective.
>
> that’s possible, I suppose …
>
>>
>> 2. They might lack a small generating set, i.e. the (oo,1)-category
>> might not be locally presentable.  Every combinatorial model category
>> (i.e. cofibrantly generated model structure on a locally presentable
>> 1-category) presents a locally presentable (oo,1)-category, and the
>> 1-category of cartesian cubical sets is certainly locally presentable,
>> but I suppose it's not obvious whether these weak factorization
>> systems are cofibrantly generated.
>
> 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 >—> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I .  In any case, a small set of generating trivial cofibrations.
>
>
> 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’s not defined over sSet, but is covered by it.
>>>
>>>> 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)-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
>>>> <Thierry...@cse.gu.se> 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’s
>>>>> paper
>>>>>
>>>>> https://arxiv.org/pdf/1704.06911
>>>>>
>>>>> that we have a model structure on cartesian cubical sets (that we can call
>>>>> “type-theoretic”
>>>>> 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 crucial
>>>>> 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”.
>>>>> 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) =
>>>>> 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’s 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 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 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.

Re: [HoTT] Quillen model structure

[Christian Sattler]

[-- Attachment #1: Type: text/plain, Size: 6203 bytes --]

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 >—>
> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for
> all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆
Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, and for trivial
cofibrations the corresponding generators Σ_I (S_{/I} hat(×)_{/I} d) with d
: I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I ×
∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → 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’s not defined over sSet, but is covered by it.
> >>
> >>> 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)-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
> >>> <Thierry...@cse.gu.se> 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’s
> >>>> paper
> >>>>
> >>>> https://arxiv.org/pdf/1704.06911
> >>>>
> >>>> that we have a model structure on cartesian cubical sets (that we can
> call
> >>>> “type-theoretic”
> >>>> 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 crucial
> >>>> 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”.
> >>>> 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) =
> >>>> 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’s 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 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 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.
>

[-- Attachment #2: Type: text/html, Size: 10550 bytes --]

Re: [HoTT] Quillen model structure

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 8272 bytes --]



> 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 <mailto: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 >—> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal 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 Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I.

sorry, I can’t read your notation.

the generating trivial cofibrations I stated are the following:

take any “indexing” map j : I^n —> I and a mono m : A >—> 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 —> I x I , so we can make a push-out product of d and m over I , say m xo d : U >—> I^n x I .  Then we forget the indexing over I to end up with the description I already gave, namely:

U =  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 —> I^n x I be the graph of j,
let g : A —> A x I be the graph of j.m, 
there is a commutative square:

		g
	A —— >	A x I
	|		|
m	|		|	m x I
	|		|
	v		v
	I^n ——>  I^n x I
	|	h
j	|
	v
	I

put the usual pushout U = I^n +_A (A x I) inside it, 
and the comprison map U —> 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 <mailto:awo...@cmu.edu>> wrote:
> >> oh, interesting!
> >> because it’s not defined over sSet, but is covered by it.
> >> 
> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu <mailto:shu...@sandiego.edu>> 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
> >>> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> 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’s
> >>>> paper
> >>>> 
> >>>> https://arxiv.org/pdf/1704.06911 <https://arxiv.org/pdf/1704.06911>
> >>>> 
> >>>> that we have a model structure on cartesian cubical sets (that we can call
> >>>> “type-theoretic”
> >>>> 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 crucial
> >>>> 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”.
> >>>> This kind of factorisation has been described in a more general framework
> >>>> in the paper of Andrew Swan
> >>>> 
> >>>> https://arxiv.org/abs/1802.07588 <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) =
> >>>> 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’s 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 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 <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
> >>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
> >>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 16396 bytes --]

Re: [HoTT] Quillen model structure

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 9849 bytes --]

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 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 >—> B x I, where m : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed family of monos, d : I —> 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)  >—>  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 Sattler <sattler....@gmail.com <mailto:sattler....@gmail.com>> wrote:
>> 
>> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu <mailto: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 >—> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal 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 Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I.
> 
> sorry, I can’t read your notation.
> 
> the generating trivial cofibrations I stated are the following:
> 
> take any “indexing” map j : I^n —> I and a mono m : A >—> 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 —> I x I , so we can make a push-out product of d and m over I , say m xo d : U >—> I^n x I .  Then we forget the indexing over I to end up with the description I already gave, namely:
> 
> U =  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 —> I^n x I be the graph of j,
> let g : A —> A x I be the graph of j.m, 
> there is a commutative square:
> 
> 		g
> 	A —— >	A x I
> 	|		|
> m	|		|	m x I
> 	|		|
> 	v		v
> 	I^n ——>  I^n x I
> 	|	h
> j	|
> 	v
> 	I
> 
> put the usual pushout U = I^n +_A (A x I) inside it, 
> and the comprison map U —> 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 <mailto:awo...@cmu.edu>> wrote:
>> >> oh, interesting!
>> >> because it’s not defined over sSet, but is covered by it.
>> >> 
>> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu <mailto:shu...@sandiego.edu>> 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
>> >>> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> 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’s
>> >>>> paper
>> >>>> 
>> >>>> https://arxiv.org/pdf/1704.06911 <https://arxiv.org/pdf/1704.06911>
>> >>>> 
>> >>>> that we have a model structure on cartesian cubical sets (that we can call
>> >>>> “type-theoretic”
>> >>>> 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 crucial
>> >>>> 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”.
>> >>>> This kind of factorisation has been described in a more general framework
>> >>>> in the paper of Andrew Swan
>> >>>> 
>> >>>> https://arxiv.org/abs/1802.07588 <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) =
>> >>>> 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’s 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 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 <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>> >>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>> >>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 18968 bytes --]

Re: [HoTT] Quillen model structure

[Christian Sattler]

[-- Attachment #1: Type: text/plain, Size: 9422 bytes --]

On Thu, Jun 14, 2018 at 3:44 PM, Steve Awodey <awo...@cmu.edu> 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 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 cofibrations are all the monos, and the fibrations
> have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m
> : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed
> family of monos, d : I —> 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)  >—>  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 <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 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 >—>
>> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for
>> all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆
> Aut(□ⁿ) and ∂□ⁿ denotes the maximal 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 Σ_I (S_{/I}
> hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G
> +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I.
>
>
> sorry, I can’t read your notation.
>
> the generating trivial cofibrations I stated are the following:
>
> take any “indexing” map j : I^n —> I and a mono m : A >—> 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 —> I x I , so we can make a push-out product
> of d and m over I , say m xo d : U >—> I^n x I .  Then we forget the
> indexing over I to end up with the description I already gave, namely:
>
> U =  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 —> I^n x I be the graph of j,
> let g : A —> A x I be the graph of j.m,
> there is a commutative square:
>
> g
> A —— > A x I
> | |
> m | | m x I
> | |
> v v
> I^n ——>  I^n x I
> | h
> j |
> v
> I
>
> put the usual pushout U = I^n +_A (A x I) inside it,
> and the comprison map U —> 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’s not defined over sSet, but is covered by it.
>> >>
>> >>> 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)-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
>> >>> <Thierry...@cse.gu.se> 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’s
>> >>>> paper
>> >>>>
>> >>>> https://arxiv.org/pdf/1704.06911
>> >>>>
>> >>>> that we have a model structure on cartesian cubical sets (that we
>> can call
>> >>>> “type-theoretic”
>> >>>> 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 crucial
>> >>>> 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”.
>> >>>> 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) =
>> >>>> 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’s 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 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 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 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.
>
>
>

[-- Attachment #2: Type: text/html, Size: 17754 bytes --]

Re: [HoTT] Quillen model structure

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 9785 bytes --]

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 >—> B x I, where m : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed family of monos, d : I —> 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)  >—>  B x I

should be:

	m xo d : B +_A (A x I) >—> B x I

Steve

> 
> 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 <mailto:awo...@cmu.edu>> wrote:
>> 
>> 
>> 
>>> On Jun 14, 2018, at 11:58 AM, Christian Sattler <sattler....@gmail.com <mailto:sattler....@gmail.com>> wrote:
>>> 
>>> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu <mailto: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 >—> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal 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 Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I.
>> 
>> sorry, I can’t read your notation.
>> 
>> the generating trivial cofibrations I stated are the following:
>> 
>> take any “indexing” map j : I^n —> I and a mono m : A >—> 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 —> I x I , so we can make a push-out product of d and m over I , say m xo d : U >—> I^n x I .  Then we forget the indexing over I to end up with the description I already gave, namely:
>> 
>> U =  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 —> I^n x I be the graph of j,
>> let g : A —> A x I be the graph of j.m, 
>> there is a commutative square:
>> 
>> 		g
>> 	A —— >	A x I
>> 	|		|
>> m	|		|	m x I
>> 	|		|
>> 	v		v
>> 	I^n ——>  I^n x I
>> 	|	h
>> j	|
>> 	v
>> 	I
>> 
>> put the usual pushout U = I^n +_A (A x I) inside it, 
>> and the comprison map U —> 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 <mailto:awo...@cmu.edu>> wrote:
>>> >> oh, interesting!
>>> >> because it’s not defined over sSet, but is covered by it.
>>> >> 
>>> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu <mailto:shu...@sandiego.edu>> 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
>>> >>> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> 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’s
>>> >>>> paper
>>> >>>> 
>>> >>>> https://arxiv.org/pdf/1704.06911 <https://arxiv.org/pdf/1704.06911>
>>> >>>> 
>>> >>>> that we have a model structure on cartesian cubical sets (that we can call
>>> >>>> “type-theoretic”
>>> >>>> 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 crucial
>>> >>>> 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”.
>>> >>>> This kind of factorisation has been described in a more general framework
>>> >>>> in the paper of Andrew Swan
>>> >>>> 
>>> >>>> https://arxiv.org/abs/1802.07588 <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) =
>>> >>>> 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’s 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 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 <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>> >>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>> >>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
> 
> 

[-- Attachment #2: Type: text/html, Size: 20848 bytes --]

Re: [HoTT] Quillen model structure

[Michael Shulman]

Okay, if the non-algebraic wfs's are cofibrantly generated in the
traditional sense, then the model category is indeed combinatorial.
Christian has also pointed out by private email that for a locally
presentable, locally cartesian closed (oo,1)-category (and, I think,
even any cocomplete locally cartesian closed one) the infinitary
aspects of the Giraud exactness axioms follow from finitary ones (for
roughly the same reasons as in the 1-categorical case) ---
specifically the "van Kampen" nature of pushouts, which should be
provable in any elementary (oo,1)-topos and thus presumably in
cartesian cubical sets.

So it seems that it's my possibility (3) that holds -- this model
structure does present a Grothendieck (oo,1)-topos.  We should be able
to work out a more traditional description of it as a left exact
localization of some (oo,1)-presheaf category by tracing through the
proofs of the presentation theorem and Giraud's theorem.


On Thu, Jun 14, 2018 at 6:44 AM, Steve Awodey <awo...@cmu.edu> 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 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 cofibrations are all the monos, and the fibrations
> have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m
> : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed
> family of monos, d : I —> 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)  >—>  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 Sattler
> <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 >—>
>> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for
>> all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆
> Aut(□ⁿ) and ∂□ⁿ denotes the maximal 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 Σ_I (S_{/I}
> hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e.
> □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I.
>
>
> sorry, I can’t read your notation.
>
> the generating trivial cofibrations I stated are the following:
>
> take any “indexing” map j : I^n —> I and a mono m : A >—> 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 —> I x I , so we can make a push-out product of d and m
> over I , say m xo d : U >—> I^n x I .  Then we forget the indexing over I to
> end up with the description I already gave, namely:
>
> U =  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 —> I^n x I be the graph of j,
> let g : A —> A x I be the graph of j.m,
> there is a commutative square:
>
> g
> A —— > A x I
> | |
> m | | m x I
> | |
> v v
> I^n ——>  I^n x I
> | h
> j |
> v
> I
>
> put the usual pushout U = I^n +_A (A x I) inside it,
> and the comprison map U —> 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’s not defined over sSet, but is covered by it.
>> >>
>> >>> 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)-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
>> >>> <Thierry...@cse.gu.se> 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’s
>> >>>> paper
>> >>>>
>> >>>> https://arxiv.org/pdf/1704.06911
>> >>>>
>> >>>> that we have a model structure on cartesian cubical sets (that we can
>> >>>> call
>> >>>> “type-theoretic”
>> >>>> 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 crucial
>> >>>> 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”.
>> >>>> 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) =
>> >>>> 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’s 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 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 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 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.

Re: [HoTT] Quillen model structure

[Steve Awodey]

> On Jun 14, 2018, at 5:47 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> Okay, if the non-algebraic wfs's are cofibrantly generated in the
> traditional sense, then the model category is indeed combinatorial.
> Christian has also pointed out by private email that for a locally
> presentable, locally cartesian closed (oo,1)-category (and, I think,
> even any cocomplete locally cartesian closed one) the infinitary
> aspects of the Giraud exactness axioms follow from finitary ones (for
> roughly the same reasons as in the 1-categorical case) ---
> specifically the "van Kampen" nature of pushouts, which should be
> provable in any elementary (oo,1)-topos and thus presumably in
> cartesian cubical sets.
> 
> So it seems that it's my possibility (3) that holds -- this model
> structure does present a Grothendieck (oo,1)-topos.  We should be able
> to work out a more traditional description of it as a left exact
> localization of some (oo,1)-presheaf category by tracing through the
> proofs of the presentation theorem and Giraud's theorem.
> 

a formidable task … and a good open problem!
thanks for clarifying.

Steve

> 
> On Thu, Jun 14, 2018 at 6:44 AM, Steve Awodey <awo...@cmu.edu> 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 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 cofibrations are all the monos, and the fibrations
>> have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m
>> : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed
>> family of monos, d : I —> 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)  >—>  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 Sattler
>> <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 >—>
>>> I^{n+1} , where the U are pushout-products of the form  I^n +_A (A x I) for
>>> all A >—> I^n cofibrant and there is some indexing I^n —> 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 ∂□ⁿ/G → □ⁿ/G where G ⊆
>> Aut(□ⁿ) and ∂□ⁿ denotes the maximal 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 Σ_I (S_{/I}
>> hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e.
>> □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I.
>> 
>> 
>> sorry, I can’t read your notation.
>> 
>> the generating trivial cofibrations I stated are the following:
>> 
>> take any “indexing” map j : I^n —> I and a mono m : A >—> 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 —> I x I , so we can make a push-out product of d and m
>> over I , say m xo d : U >—> I^n x I .  Then we forget the indexing over I to
>> end up with the description I already gave, namely:
>> 
>> U =  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 —> I^n x I be the graph of j,
>> let g : A —> A x I be the graph of j.m,
>> there is a commutative square:
>> 
>> g
>> A —— > A x I
>> | |
>> m | | m x I
>> | |
>> v v
>> I^n ——>  I^n x I
>> | h
>> j |
>> v
>> I
>> 
>> put the usual pushout U = I^n +_A (A x I) inside it,
>> and the comprison map U —> 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’s not defined over sSet, but is covered by it.
>>>>> 
>>>>>> 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)-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
>>>>>> <Thierry...@cse.gu.se> 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’s
>>>>>>> paper
>>>>>>> 
>>>>>>> https://arxiv.org/pdf/1704.06911
>>>>>>> 
>>>>>>> that we have a model structure on cartesian cubical sets (that we can
>>>>>>> call
>>>>>>> “type-theoretic”
>>>>>>> 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 crucial
>>>>>>> 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”.
>>>>>>> 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) =
>>>>>>> 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’s 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 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 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 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.

Re: [HoTT] Quillen model structure

[Richard Williamson]

Dear Thierry,

Forgive me for not quite having an overview of exactly what has
been done. My interest here is in how the model structure you
have constructed compares with Cisinski's work. For example, I
would expect that the category of cartesian cubical sets is a
test category. Indeed, I would expect that more or less exactly
the same technique as in 8.4 of Les préfaisceaux comme ... goes
through to prove this. And I would expect that one can put a
model structure on in the same way.

Now, I believe I saw in some slides that that your model
structure coincides with the Cisinski one. But this does not seem
compatible with my expectations above, because then it is
certainly Quillen equivalent to the Serre model structure on
topological spaces (or whatever).

Thus my questions:

1) Have I misinterpreted the slides or some other aspect of your
work?

2) If not, where exactly do Cisinski's techniques fail?

Best wishes,
Richard

Re: [HoTT] Quillen model structure

[Steve Awodey]

Dear Richard,

I believe the answer to (1) is yes : - )

The main point of Thierry's note is that the so-called “type theoretic model structure” on cartesian cubical sets (which as Thierry clearly says is essentially the work of Christian Sattler) is *not* equivalent to the one arising from the (well-known) fact that the cartesian cube category is a (strict) test category.

Where exactly this conflicts with a Cisinski style approach is a distinct issue, I think — maybe that’s your (2)?

Regards,

Steve 


> On Jun 14, 2018, at 8:39 PM, Richard Williamson <rwilli...@gmail.com> wrote:
> 
> Dear Thierry,
> 
> Forgive me for not quite having an overview of exactly what has
> been done. My interest here is in how the model structure you
> have constructed compares with Cisinski's work. For example, I
> would expect that the category of cartesian cubical sets is a
> test category. Indeed, I would expect that more or less exactly
> the same technique as in 8.4 of Les préfaisceaux comme ... goes
> through to prove this. And I would expect that one can put a
> model structure on in the same way.
> 
> Now, I believe I saw in some slides that that your model
> structure coincides with the Cisinski one. But this does not seem
> compatible with my expectations above, because then it is
> certainly Quillen equivalent to the Serre model structure on
> topological spaces (or whatever).
> 
> Thus my questions:
> 
> 1) Have I misinterpreted the slides or some other aspect of your
> work?
> 
> 2) If not, where exactly do Cisinski's techniques fail?
> 
> Best wishes,
> Richard
> 
> -- 
> 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.

Re: [HoTT] Quillen model structure

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 4582 bytes --]


Dear Richard,

 The model structure is  not due to me but to Christian Sattler, and is explained in Section 2
of

 https://arxiv.org/pdf/1704.06911

(where I did some joint work is in the constructive argument that we have fibrant universes).

Cisinski defines in his book a model structure on presheaves where cofibrations
are monos. In order to define the model structure, one needs a “cylindre fonctoriel”
that we can define from a “segment”  II (a presheaf with two global distinct elements 0 and 1)
Exemple 1.3.8. We further need a “donnee homotopique”  Definition 1.3.14, given by a
set of monomorphism S. We only consider here the least case where S = empty set. From
this we can define a notion of anodyne map.
Given II and S, Cisinski explains then how to define a Quillen model structure Theorem 1.3.22
where

 -the cofibrations are the monomorphism
 -the anodyne maps are generated by open box inclusion, A x II \cup B x b -> B x II for A -> B
mono and b = 0,1
 -the fibrant objects are the ones having the extension property w.r.t. anodyne maps
 -the -naive- fibrations are the maps having the right lifting properties w.r.t. anodyne maps
(so a map X -> 1 is a naive fibration iff X if fibrant)
 -the weak equivalence are the maps A -> B such that for any fibrant X, the map
X^B -> X^A is a homotopy equivalence (w.r.t. the choice of the interval II)
 -the fibrations are the maps having the right lifting properties w.r.t. maps that are monos
and weak equivalence

 W.r.t. the slides at

http://uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Coquand-2018-05-24-HoTTEST.pdf

if we limit ourselves to the case where the base category is the Lawvere theory of
distributive lattices, or de Morgan algebra, or Boolean algebra and we take the fibrations
as defined page 13, we get the same notion as Cisinski -naive- fibrations.

 It follows from Section 2 of Christian’s paper above that we also get a model structure
having exactly this notion of fibration (and where cofibrations are monos).

 We then have a priori two model structures on these presheaves.
 They have the same notion
of fibrant objects and cofibrations. It follows then from André Joyal’s result
(Riehl Categorical Model Theory, Theorem 15.3.1) that we actually the -same- model
structure.

 It then follows that in these cases, the Cisinski model structure is -complete-
(Definition 1.3.48).

 In the case of de Morgan algebra, or distributive lattice, we have a geometric realisation map.
However in the case of de Morgan algebra, we don’t have that this map is a Quillen equivalence
as shown by Christian: if we take L to be the quotient of II by the de Morgan reversal operation
then the geometric realisation of L is contractible, but it can be shown that the map L -> 1
is not an equivalence for Cisinski (= Christian in this case) model structure.

 It is an open problem what happens for distributive lattices.

 I am not a specialist of test categories but my understanding is that all these categories
(Lawvere theory of distributive lattices, de Morgan algebra, algebra with two constants 0,1)
are test categories, but it is not clear if the general notion of weak equivalence we get
from the theory of test category coincide with the one of Cisinski model structure
(and indeed it will not coincide for de Morgan algebra and Boolean algebra, and this
is open for distributive lattices),

 Best regards,
 Thierry








On 14 Jun 2018, at 20:39, Richard Williamson <rwilli...@gmail.com<mailto:rwilli...@gmail.com>> wrote:

Dear Thierry,

Forgive me for not quite having an overview of exactly what has
been done. My interest here is in how the model structure you
have constructed compares with Cisinski's work. For example, I
would expect that the category of cartesian cubical sets is a
test category. Indeed, I would expect that more or less exactly
the same technique as in 8.4 of Les préfaisceaux comme ... goes
through to prove this. And I would expect that one can put a
model structure on in the same way.

Now, I believe I saw in some slides that that your model
structure coincides with the Cisinski one. But this does not seem
compatible with my expectations above, because then it is
certainly Quillen equivalent to the Serre model structure on
topological spaces (or whatever).

Thus my questions:

1) Have I misinterpreted the slides or some other aspect of your
work?

2) If not, where exactly do Cisinski's techniques fail?

Best wishes,
Richard


[-- Attachment #2: Type: text/html, Size: 7455 bytes --]

Re: [HoTT] Quillen model structure, PS

[Thierry Coquand]

  I wrote

——————

if we limit ourselves to the case where the base category is the Lawvere theory of
distributive lattices, or de Morgan algebra, or Boolean algebra and we take the fibrations
as defined page 13, we get the same notion as Cisinski -naive- fibrations.

——————

 I should have added that this is not completely trivial: it amounts to the fact that to 
have the -uniform- right lifting filling property w.r.t. any open box inclusion

 A x II \cup B x b    ->     B  x II             where B is -representable-, A -> B mono

(where we have a choice of lifting that are natural w.r.t. map B’ -> B between
representables)

is -equivalent- to having the (non necessarily uniform) right lifting property 
w.r.t. -any- open box inclusion

 A x II \cup B x b    ->     B  x II             B arbitrary, A -> B mono



  The same holds (and is either to check) for trivial fibrations: to have the uniform
right lifting property w.r.t. A -> B mono, B representable is equivalent to having
the right lifting property w.r.t. an arbitrary mono.

 Best regards,
 Thierry



> On 14 Jun 2018, at 20:39, Richard Williamson <rwilli...@gmail.com> wrote:
> 
> Dear Thierry,
> 
> Forgive me for not quite having an overview of exactly what has
> been done. My interest here is in how the model structure you
> have constructed compares with Cisinski's work. For example, I
> would expect that the category of cartesian cubical sets is a
> test category. Indeed, I would expect that more or less exactly
> the same technique as in 8.4 of Les préfaisceaux comme ... goes
> through to prove this. And I would expect that one can put a
> model structure on in the same way.
> 
> Now, I believe I saw in some slides that that your model
> structure coincides with the Cisinski one. But this does not seem
> compatible with my expectations above, because then it is
> certainly Quillen equivalent to the Serre model structure on
> topological spaces (or whatever).
> 
> Thus my questions:
> 
> 1) Have I misinterpreted the slides or some other aspect of your
> work?
> 
> 2) If not, where exactly do Cisinski's techniques fail?
> 
> Best wishes,
> Richard

Re: [HoTT] Quillen model structure

[Richard Williamson]

Dear Steve and Thierry,

> I believe the answer to (1) is yes : - )

Hehe, that is very likely, and I will be happy to acknowledge it!
:-)

> Where exactly this conflicts with a Cisinski style approach is
> a distinct issue, I think — maybe that’s your (2)?

Exactly. It has been a little while since I was really working on
this stuff, so I could be forgetting something, but as far as I
know the test model structure on cartesian cubical sets is
exactly the one coming from the theorem of Cisinski that Thierry
cites using the obvious cylinder, and with empty S. Now, Thierry
also says, I believe, that this model structure is the same as
the one of Christian Sattler. How can this be?!

Presumably I have something wrong, but I do not see yet what it
is after the replies so far.

Best wishes,
Richard

Re: [HoTT] Quillen model structure

[Ulrik Buchholtz]

[-- Attachment #1.1: Type: text/plain, Size: 1405 bytes --]


>
> Exactly. It has been a little while since I was really working on 
> this stuff, so I could be forgetting something, but as far as I 
> know the test model structure on cartesian cubical sets is 
> exactly the one coming from the theorem of Cisinski that Thierry 
> cites using the obvious cylinder, and with empty S. Now, Thierry 
> also says, I believe, that this model structure is the same as 
> the one of Christian Sattler. How can this be?! 
>

The weak equivalences of the test model structure form the least _regular_ 
test localizer.

The identity adjunction gives a left Quillen functor from the type 
theoretic model structure to the test model structure, but this is only an 
equivalence when the weak equivalences of the former form a regular 
localizer (meaning: every presheaf is the homotopy colimit of its category 
of elements).

BTW, for de Morgan (or Kleene) cubes, geometric realization is not even a 
left Quillen adjunct for the type theoretic model structure with all 
(decidable) monos as cofibrations, since the geometric realization of the 
inclusion of the union of the two diagonals into the square is not a 
topological cofibration (it's not even injective). There are “smaller” type 
theoretic model structures with fewer cofibrations, but even for those, 
geometric realization cannot be a Quillen equivalence.

Best wishes,
Ulrik


[-- Attachment #1.2: Type: text/html, Size: 1646 bytes --]

Re: [HoTT] Quillen model structure

[Richard Williamson]

> Exactly. It has been a little while since I was really working on
> this stuff, so I could be forgetting something, but as far as I
> know the test model structure on cartesian cubical sets is
> exactly the one coming from the theorem of Cisinski that Thierry
> cites using the obvious cylinder, and with empty S. Now, Thierry
> also says, I believe, that this model structure is the same as
> the one of Christian Sattler. How can this be?!

I was mis-remembering. If one looks at 8.4.34 - 8.4.38 in Les
préfaisceaux ..., one sees that S is taken (of course, now that I
think properly about it!) to be the (non-empty!) set of horn
inclusions.

In summary, the difference, from the point of view of Cisinski's
theory, between the type-theoretic model structure and the test
model structure seems to be precisely the choice of S.

Thank you to all!