From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a19:1659:: with SMTP id m86-v6mr377963lfi.39.1528922991607; Wed, 13 Jun 2018 13:49:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:c44f:: with SMTP id u76-v6ls573413lff.4.gmail; Wed, 13 Jun 2018 13:49:50 -0700 (PDT) X-Received: by 2002:a19:8fc6:: with SMTP id s67-v6mr349143lfk.10.1528922990147; Wed, 13 Jun 2018 13:49:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528922990; cv=none; d=google.com; s=arc-20160816; b=KFIIpA4Hs8D7ZB7hCkm2gI+6ttiPODT4wvlS3q+D9KzjF7aSiegHKEli6x7SKGjr2z 5VBWe6i/eUrQX1GnSDf9vdiBSIAnmw/7Fru+8Tj5hUOo6F4Ujm9fnndwgZcBiwCmJW9U COfPDcGX8Zs3jEiX7Zqic/sifyAXQy8W3bINb3qVZiq0rt8UKP8XEmooP3zbkUMl+g6z cdOo1SMw9ulLzruOBlf07aUlveqxcXIEWS1UbYWEnOCCWQ7uLw3GTSAV6zuD1JosWNYK lalT0DGz7bsEF6w02PDIZkukrOb8TT07TPjctkYXLQaOSwAnet03N+Oz9rQ8oCuwddJs NABA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature :arc-authentication-results; bh=QUC/C065E3vZcWnu0+BXNOYK+CZ8/Bl25nkEiP4A+Co=; b=cOMiM+oULPa6Eoqn4l56VacMdZVRyYr0jbE10S8i1m5wM5Y6/iS80UriStZ8fpfnio xqYxzkVNDWoYimYqHg5hveriAcOuzIwm5vXXQYNad1qiw0XglYj5dona3eO8wYQPxxgu BnTKzN3qNbNwPJsKUbEmMsVKefypllVFy4VryeF8o5powvxLw/D9AYlTF5tFcY3LZYdh 7GKe3K3o2mvUXMGjsXJJROKSjVv1ymtXY4my73hxQlDkTgFtwRngqDwL5cc/qs4AqaK1 Jrie3chQwMV6ZTPvmAHqD5PtMHmVl9eDlrJzMwXhyhUkTc3uu10y7IBBzOcBR880Oyu1 eDwQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=f7LsjHx2; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22c as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-wm0-x22c.google.com (mail-wm0-x22c.google.com. [2a00:1450:400c:c09::22c]) by gmr-mx.google.com with ESMTPS id l24-v6si145902lja.1.2018.06.13.13.49.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Jun 2018 13:49:50 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22c as permitted sender) client-ip=2a00:1450:400c:c09::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=f7LsjHx2; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c09::22c as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-wm0-x22c.google.com with SMTP id v131-v6so7905429wma.1 for ; Wed, 13 Jun 2018 13:49:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=QUC/C065E3vZcWnu0+BXNOYK+CZ8/Bl25nkEiP4A+Co=; b=f7LsjHx2sDkiijTW/eVmnhy6+AYMX7VgC8oPb9Drt7uGKo8QIBmk+s4PPfopZsgANo qqDsKxfeLvIPQBarV3Ib0b7fCG+mCj0C4aJeJ/Jg1FlgxYTIvgbr4BQPIjGYY6Vu19oc aLyG38KWCtrsaRzXuuGANJmS8JYqmyJD0P3nq5GNmnChD5VOfDCx6VXzbZIG0Y3tiGxn WeO9kCf+9tbrPTmthh75sIl4udW1FbzBh8nZj3s4wIK9XxXM4+YRXGmIQZpfS4XGK0rs qiOWxsszvkuVuvADx7hZOOIUJAFZRFtNKKwYozkwXphLFoHULFJohmp+nAHJC77OypX3 V4Ag== X-Gm-Message-State: APt69E1Y4m85fVC+75aGhmV5l8LjaGOHGRABAnOdF51xDFCX+p4BKRkL 6rg+rqT+Uu2m1Y+kq6xb/3OyhencOaI= X-Received: by 2002:a1c:d509:: with SMTP id m9-v6mr4729001wmg.69.1528922989874; Wed, 13 Jun 2018 13:49:49 -0700 (PDT) Return-Path: Received: from ?IPv6:2003:e2:af39:b600:5186:dcde:9c1:2ced? (p200300E2AF39B6005186DCDE09C12CED.dip0.t-ipconnect.de. [2003:e2:af39:b600:5186:dcde:9c1:2ced]) by smtp.gmail.com with ESMTPSA id d90-v6sm5329569wmi.26.2018.06.13.13.49.49 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Jun 2018 13:49:49 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 11.3 \(3445.6.18\)) Subject: Re: [HoTT] Quillen model structure From: Steve Awodey In-Reply-To: Date: Wed, 13 Jun 2018 22:50:08 +0200 Cc: Thierry Coquand , Homotopy Theory Content-Transfer-Encoding: quoted-printable Message-Id: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> References: To: Michael Shulman X-Mailer: Apple Mail (2.3445.6.18) oh, interesting! because it=E2=80=99s not defined over sSet, but is covered by it. > On Jun 13, 2018, at 10:33 PM, Michael Shulman wrote= : >=20 > 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? >=20 > On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand > wrote: >> The attached note contains two connected results: >>=20 >> (1) a concrete description of the trivial cofibration-fibration >> factorisation for cartesian >> cubical sets >>=20 >> It follows from this using results of section 2 of Christian Sattler=E2= =80=99s >> paper >>=20 >> https://arxiv.org/pdf/1704.06911 >>=20 >> that we have a model structure on cartesian cubical sets (that we can ca= ll >> =E2=80=9Ctype-theoretic=E2=80=9D >> since it is built on ideas coming from type theory), which can be done i= n a >> constructive >> setting. The fibrant objects of this model structure form a model of typ= e >> 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). >>=20 >> I described essentially the same argument for factorisation in a messag= e >> 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=E2=80=9D. >> This kind of factorisation has been described in a more general framewor= k >> in the paper of Andrew Swan >>=20 >> https://arxiv.org/abs/1802.07588 >>=20 >>=20 >>=20 >> Since there is a canonical geometric realisation of cartesian cubical se= ts >> (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 >>=20 >> (2) the geometric realisation map is -not- a Quillen equivalence. >>=20 >> 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) =3D >> 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. >>=20 >> 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=E2=80=99s argume= nt 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. >>=20 >> Note that this implies that the canonical map Cartesian cubes -> Dedek= ind >> 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 struc= ture >> obtained by transfer >> and described at >>=20 >> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>=20 >> is not equivalent to the type-theoretic model structure. >>=20 >> Thierry >>=20 >> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussio= ns >> about this last week in Bonn. >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 > --=20 > 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.