89 views

Skip to first unread message

Jun 10, 2018, 9:31:22 AM6/10/18

to Homotopy Theory

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

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

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

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.

Jun 11, 2018, 4:46:54 AM6/11/18

to Hiroyuki Miyoshi, Homotopy Theory

Hello

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

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.

Jun 13, 2018, 4:34:17 PM6/13/18

to Thierry Coquand, Homotopy Theory

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?

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?

Jun 13, 2018, 4:49:51 PM6/13/18

to Michael Shulman, Thierry Coquand, Homotopy Theory

oh, interesting!

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

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

Jun 13, 2018, 6:00:30 PM6/13/18

to Steve Awodey, Thierry Coquand, Homotopy Theory

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.

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

Jun 14, 2018, 5:28:08 AM6/14/18

to Michael Shulman, Thierry Coquand, Homotopy Theory

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

>

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

- 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

Jun 14, 2018, 5:48:27 AM6/14/18

to Steve Awodey, nicolas tabareau, Michael Shulman, Thierry Coquand, Homotopy Theory

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.

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.

Jun 14, 2018, 5:58:26 AM6/14/18

to Steve Awodey, Michael Shulman, Thierry Coquand, Homotopy Theory

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.

Jun 14, 2018, 6:27:53 AM6/14/18

to Christian Sattler, Michael Shulman, Thierry Coquand, Homotopy Theory

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.

Jun 14, 2018, 9:45:01 AM6/14/18

to Christian Sattler, Michael Shulman, Thierry Coquand, Homotopy Theory

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

Jun 14, 2018, 10:52:33 AM6/14/18

to Steve Awodey, Michael Shulman, Thierry Coquand, Homotopy Theory

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-productm xo d : I^n +_A (A x I) >—> B x Iis 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.

--

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.

Jun 14, 2018, 11:41:55 AM6/14/18

to Homotopy Theory

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

Jun 14, 2018, 11:48:12 AM6/14/18

to Steve Awodey, Christian Sattler, Thierry Coquand, Homotopy Theory

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.

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.

Jun 14, 2018, 12:01:45 PM6/14/18

to Michael Shulman, Christian Sattler, Thierry Coquand, Homotopy Theory

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

>

thanks for clarifying.

Steve

Jun 14, 2018, 2:40:02 PM6/14/18

to Thierry Coquand, Homotopy Theory

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

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

Jun 14, 2018, 3:14:27 PM6/14/18

to Richard Williamson, Thierry Coquand, Homotopy Theory

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

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

Jun 14, 2018, 3:16:04 PM6/14/18

to Richard Williamson, Homotopy Theory

Dear Richard,

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

of

(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

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

Jun 14, 2018, 3:35:45 PM6/14/18

to Richard Williamson, Homotopy Theory

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.

Jun 14, 2018, 4:15:06 PM6/14/18

to Steve Awodey, Thierry Coquand, Homotopy Theory

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

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

:-)

> Where exactly this conflicts with a Cisinski style approach is

> a distinct issue, I think — maybe that’s your (2)?

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

Jun 14, 2018, 4:32:05 PM6/14/18

to Homotopy Type Theory

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

Jun 14, 2018, 5:07:59 PM6/14/18

to Steve Awodey, Thierry Coquand, Homotopy Theory

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

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!

Reply all

Reply to author

Forward

0 new messages