From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a6b:3ce:: with SMTP id e75-v6mr2571842ioi.93.1528922057361; Wed, 13 Jun 2018 13:34:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:c407:: with SMTP id y7-v6ls982189ioa.5.gmail; Wed, 13 Jun 2018 13:34:16 -0700 (PDT) X-Received: by 2002:a6b:1985:: with SMTP id 127-v6mr2829477ioz.136.1528922056475; Wed, 13 Jun 2018 13:34:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528922056; cv=none; d=google.com; s=arc-20160816; b=rGjLLdBQpd5HamV3ucqmcyIwRar1XhIaB8Un/LUBdduW2RW3BAeiPfbBPrtB9q/hTj JLKIDS54RjpT4brSo/ei2RpgorA2krKj6oKY+Yu/SURN8+/oagRyzqoJSaMyI2Ijwut8 jHDD/BrLcg2hbzTn5DTlhv0W93d0Bo0+nYEGqtpviE5vvsYGFsQf1ll7d+8sxsYS8Q65 +CJ00Kf+BbG5H2YZ9XVn88kil2lFLPS0g35Oh7xfZYPc1N3A5GCeeHt5QVFYMDPxd4vU yXI+gQ/PngRxhG5zJJXFkHhfdODPG9GRKmpaSDARfHH4+bH4XSHgAYHB48Vs7W9K5XP/ D6vg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=wdmF1bahnybk01eTeh+VsFeovF/5V6ARM+nfp0lG6Vg=; b=brbHGUrGaj1tOUihgE7ltvs6FgF0LaCLGIcBaipJOZNsZK6kF5uqEPYuh/rWRTJMs7 K5hnUPoOl/b+pZqdpqU2hN7EI1vrPOdqZoyr3/R0i+koZLgPs/jQ8bFHOIWss8I8Bkr6 WkKXk/acL9qlba2fAwxc2WvVYIWhiOY0IYbBt/YOo9iGx4cK25DobMJZbjPdtJTiUYvf uyk6coJ76m+p6atTvhrEWBNw3xG+2iIBPM3cWIBdCWX1RvWg+bSaQMeUDbQbJ+CjWKGM 2RxR2dX47RIMeOOa2UnVXKe110BrJ1+oYJj6mlNy9Wd+ygzsWQg6KQrx9UD4UmkQzKFS 2jsA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WGNF21zG; spf=neutral (google.com: 2607:f8b0:4002:c09::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22a.google.com (mail-yb0-x22a.google.com. [2607:f8b0:4002:c09::22a]) by gmr-mx.google.com with ESMTPS id t2-v6si247822iog.2.2018.06.13.13.34.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Jun 2018 13:34:16 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22a is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WGNF21zG; spf=neutral (google.com: 2607:f8b0:4002:c09::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22a.google.com with SMTP id x128-v6so1416361ybg.3 for ; Wed, 13 Jun 2018 13:34:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=wdmF1bahnybk01eTeh+VsFeovF/5V6ARM+nfp0lG6Vg=; b=WGNF21zGvB3sX1Cja1rNouemE8RN8OjXcjXydiqs8qat/X8U+lfI5lQ2H78JRh3foO kCI6A0MOSHtJU1FSM8N+hshI6T9/thiQE7eyjJfdErX7Dfuts6fYnnXH58ryzQEXVShU XC0GsMHPvsJSoSDv18s61vB9MHoLZv8z7nrSTvVjMZYG6g5HuC3z47K0HbBtAoN0Y9Jh VQ9GvaDIdY7cfbZ+fTEAzhzryJtE11Y/dEL9dHcnSjNjg02R1AoFhMPyi98jMDX4PNmx GRGNbRmonO0AP2cid16Zjb5oC4R64uAEGemy9hzY98x9dpOT+ZmATHURd631zaLW5ENR 80NQ== X-Gm-Message-State: APt69E3HQu9BA2cFkae1ojPgpqE6rji+u4/itqEtSt6gQwo73C6m3Xzg c14HDud8/9iC1n8pGWaq5IIhItam X-Received: by 2002:a25:d28b:: with SMTP id j133-v6mr3327226ybg.340.1528922055862; Wed, 13 Jun 2018 13:34:15 -0700 (PDT) Return-Path: Received: from mail-yb0-f182.google.com (mail-yb0-f182.google.com. [209.85.213.182]) by smtp.gmail.com with ESMTPSA id c20-v6sm566689ywk.90.2018.06.13.13.34.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Jun 2018 13:34:14 -0700 (PDT) Received: by mail-yb0-f182.google.com with SMTP id u11-v6so1408515ybi.8 for ; Wed, 13 Jun 2018 13:34:14 -0700 (PDT) X-Received: by 2002:a25:bfc4:: with SMTP id q4-v6mr3241685ybm.165.1528922054357; Wed, 13 Jun 2018 13:34:14 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Wed, 13 Jun 2018 13:33:53 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Wed, 13 Jun 2018 13:33:53 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Quillen model structure To: Thierry Coquand Cc: Homotopy Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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=E2= =80=99s > paper > > https://arxiv.org/pdf/1704.06911 > > that we have a model structure on cartesian cubical sets (that we can cal= l > =E2=80=9Ctype-theoretic=E2=80=9D > 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 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 > > https://arxiv.org/abs/1802.07588 > > > > 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 i= s 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 t= ype > 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. > > 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 argumen= t 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 -> 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 struct= ure > 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 discussion= s > 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. > For more options, visit https://groups.google.com/d/optout.