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

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