Re: [HoTT] Quillen model structure

[Thierry Coquand <Thierry...@cse.gu.se>]

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