Quillen model structure

[Thierry Coquand]

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.

[Thierry Coquand]

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


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

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

[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?

[Steve Awodey]

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

[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.

[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

[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.

[Christian Sattler]

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

>>>> email to HomotopyTypeTheory+unsub...@googlegroups.com.

>>>> For more options, visit https://groups.google.com/d/optout.
>>>
>>> --
>>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

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

[Steve Awodey]

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

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Steve Awodey]

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

[Christian Sattler]

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

Steve

>>>> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

>>>> For more options, visit https://groups.google.com/d/optout.
>>>
>>> --
>>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

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

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Steve Awodey]

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

[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.

[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

[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

[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

[Thierry Coquand]

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

[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:
>

[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

[Ulrik Buchholtz]

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

[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!