From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a2e:9754:: with SMTP id f20-v6mr216938ljj.21.1529003667090; Thu, 14 Jun 2018 12:14:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:780f:: with SMTP id t15-v6ls953963ljc.2.gmail; Thu, 14 Jun 2018 12:14:26 -0700 (PDT) X-Received: by 2002:a2e:8958:: with SMTP id b24-v6mr221298ljk.38.1529003666097; Thu, 14 Jun 2018 12:14:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1529003666; cv=none; d=google.com; s=arc-20160816; b=AykJl0mrLXnSjivjuBKKg8gHDqBM8CKaPpy0BfdGnCTBrBXg6MqRw1WA5FC7DgcP5M DhKTelh9uwX/z858ZepkNBDz6UonOA+4jhQp1YU0rTyBsGCfF5yAzYBXYch7jYpHp0Jp HqNCh6gmhuAvtiDNNj2NQX9Ecv2lllHQflV/W7e2CH2qZrr81jxqJshNw+0o4jLq9Kt+ NdBo9Zceuq3lcBaLwF9KAMHr1VZhuEiWl6BzjE5V+MjW/lSp0m3+90wZeXPmeVIUr/w2 ukKU6Z6/cKQOv0Vo1cSGVUWxt35VefY0LqIZGDo+0Rb6StVegaBzoS3E3VEENDNNwhNG m1CA== 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=IESd52GAp5uA3mJbBM+Jmo8MbQMFDq8FqzEwsfsjHV0=; b=ZvWAh5C3LdM5NFDIERW7WPJCTtHRdfInk9gpTxhMrBJ+2QEOlh+b6Q7gGlfnsMZR4v 5KnA3S0uHjpDpJVcv4M+RyhDiYpvqAI12hGmDoJSp9mwsozOJnl1U56LpSKm/zgcRjVf 78MtN8/vs5BjO+nounsAYYqLYvetrHB4/TANoHvovi9+Hky51f9kR/L85gokxR1EmoAB cklWydaDYL7/B7s+0Z3aSpIHgosSgPtaIQ8wqzkSMNym00g7L9pyqDCk3FoZno0Y2/88 SjZ0iQgDbFusl77L9J8wA62sGlz0xP6232A8J2mcGk9XtjI4npx/j8H9T4ovd8xl/4SK d0+g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=xOAgVYBu; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::230 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-wr0-x230.google.com (mail-wr0-x230.google.com. [2a00:1450:400c:c0c::230]) by gmr-mx.google.com with ESMTPS id y7-v6si202988lfd.4.2018.06.14.12.14.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 12:14:26 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::230 as permitted sender) client-ip=2a00:1450:400c:c0c::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=xOAgVYBu; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2a00:1450:400c:c0c::230 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-wr0-x230.google.com with SMTP id o12-v6so7531680wrm.12 for ; Thu, 14 Jun 2018 12:14:26 -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=IESd52GAp5uA3mJbBM+Jmo8MbQMFDq8FqzEwsfsjHV0=; b=xOAgVYBuriBZ0iutTMEpblx7ySgCXkpyFzSKz4PpMCVG9mqyBqFXhb7B2Z2es95B5h Q0qbD06FX48o+L/2n0K/H65L9L7V223NMZ1KjiNp78pe3aLSn6o5tif2tXwXI1D5xxqw FEzpyZCExTUma0roQhGlbffNdAclHFDrN6qAKl6EKroeXQakuuoO6+XRgkdPPBqoThnj zrcVAjl57YGkf083Z2ljnVLh/Py2NXEeoVFwoua7TdW4I+5Tpqc4+x8KqnhKhDvhuxtL 2+3ySfCTo5WMGh/wU12t06jRs4U5qtv+aA2wOWKEUwt5f1GXXFbcpoJORCbprdrhiFgN IEcw== X-Gm-Message-State: APt69E2gls3ge5LMnqkIsw/5g+RCxF2MMakUiLYTHCGDx6WFTUaIjvi+ wK6V/bEPSQw4HayWUG70ySl8KQ== X-Received: by 2002:adf:f811:: with SMTP id s17-v6mr3234966wrp.172.1529003665515; Thu, 14 Jun 2018 12:14:25 -0700 (PDT) Return-Path: Received: from ?IPv6:2003:e2:af2e:8400:ec11:d9b5:73b8:ff64? (p200300E2AF2E8400EC11D9B573B8FF64.dip0.t-ipconnect.de. [2003:e2:af2e:8400:ec11:d9b5:73b8:ff64]) by smtp.gmail.com with ESMTPSA id w15-v6sm9717718wro.52.2018.06.14.12.14.24 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 12:14:24 -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: <20180614183959.GA1401@richard.richard> Date: Thu, 14 Jun 2018 21:14:45 +0200 Cc: Thierry Coquand , Homotopy Theory Content-Transfer-Encoding: quoted-printable Message-Id: <54A8E26C-ECF8-441A-AC3F-7643DA47C3FE@cmu.edu> References: <20180614183959.GA1401@richard.richard> To: Richard Williamson X-Mailer: Apple Mail (2.3445.6.18) Dear Richard, I believe the answer to (1) is yes : - ) The main point of Thierry's note is that the so-called =E2=80=9Ctype theore= tic model structure=E2=80=9D on cartesian cubical sets (which as Thierry cl= early says is essentially the work of Christian Sattler) is *not* equivalen= t to the one arising from the (well-known) fact that the cartesian cube cat= egory is a (strict) test category. Where exactly this conflicts with a Cisinski style approach is a distinct i= ssue, I think =E2=80=94 maybe that=E2=80=99s your (2)? Regards, Steve=20 > On Jun 14, 2018, at 8:39 PM, Richard Williamson wro= te: >=20 > Dear Thierry, >=20 > 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=C3=A9faisceaux comme ... goes > through to prove this. And I would expect that one can put a > model structure on in the same way. >=20 > 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). >=20 > Thus my questions: >=20 > 1) Have I misinterpreted the slides or some other aspect of your > work? >=20 > 2) If not, where exactly do Cisinski's techniques fail? >=20 > Best wishes, > Richard >=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.