From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:f108:: with SMTP id p8-v6mr439332wmh.0.1529010479620; Thu, 14 Jun 2018 14:07:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:7c18:: with SMTP id x24-v6ls31753wmc.2.gmail; Thu, 14 Jun 2018 14:07:58 -0700 (PDT) X-Received: by 2002:a1c:6507:: with SMTP id z7-v6mr394582wmb.12.1529010478897; Thu, 14 Jun 2018 14:07:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1529010478; cv=none; d=google.com; s=arc-20160816; b=mo+wZqy4mJr5SN1LuN62Dk7qJdFszHmZjzuFojFWUkD8aC1EDcKYuhLW0Q88uzAqyv yow9MVy7/vnPcpW/ufr712UssyIGZnN7zO2zgfyQmCIUL2NxbTtHbDCFQbTAjr+r8Ao3 YU23T4tAE3WEhPkEXatvLJgSWjQ2aeut0kEwDo2gn4/zB3jeZPj2F9mHd2I76H2rb8Hy mHT+ga7glZLw9HXmo5727LtLwLTcj4J84EgqLaBf5kCCdFIIjxGJlBc+OSl6M4Iqzgsu 97xCVw+dbwj/G+v5JLUeBfpJMDEJAChj3yc+tLKaFeE2Py2E4R1IBasUa/G/K8xutcQ2 /5nw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-transfer-encoding :content-disposition:mime-version:references:message-id:subject:cc :to:from:date:dkim-signature:arc-authentication-results; bh=VvXjbJMi1USKWurGmLu4vx0yNz7EHPPLeXkQzLvNmjw=; b=rmenYpLnJNCVXk3nCVfEiTKNKP8HBRs1FJQcD06Ws1/kMIRpjEN1S2RfPCUdeKrJgE gH1WPG7QXaoPWNStB/5wWBqILqTv8fYW/dAdrdmCOkh5uzdNWdRcU6i/dZOimy+QcTTY o5Z2s2gtEmxufabFnT7OIuSM4rDL+5uqq1QEuf2wlSAoYqUAaFQHQHFd7kW5BIFGKGeM TWr/lRkRRYBxPBoqM96GXHtY4BS/wSXk7jdE4aQJ+nL7aoe0IZLQh3XCWA8GrPuvGk6w kODyJR5u63ogg1+iGjP1c9qKWvYJjxktRkGnenm74BrsSKMOoZnOhFzttJXyLoylortE 2UHA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=sYS+JsTe; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::234 as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-lf0-x234.google.com (mail-lf0-x234.google.com. [2a00:1450:4010:c07::234]) by gmr-mx.google.com with ESMTPS id v25-v6si85074wmh.2.2018.06.14.14.07.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 14:07:58 -0700 (PDT) Received-SPF: pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::234 as permitted sender) client-ip=2a00:1450:4010:c07::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=sYS+JsTe; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::234 as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-lf0-x234.google.com with SMTP id g21-v6so11560098lfb.4 for ; Thu, 14 Jun 2018 14:07:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:content-transfer-encoding:in-reply-to :user-agent; bh=VvXjbJMi1USKWurGmLu4vx0yNz7EHPPLeXkQzLvNmjw=; b=sYS+JsTeS5Djyl+3H+/F/femA0+SuaFceEYQPLrb8D4phZwl9ruI/+42wKGaWlBxs9 25gyt+y/TrbO2pwnHdAZIebUi546BjYspRvJaPhAdbBk9Lg+YK5/MB4X6o9p1EQwKFrh ZbUIm6EV6seCJM+14ytWy0oveS4baJdD0Fg2RXPvcXOH4d6h4XadvrVI8sgZrdiw/+CX OkHHfiDoUfwRgfeiYJ0d24kdigVmVRe1wpQWyF5/Xqql6ujNfSKnNIhDeFuCr7Jq/idR t85XGTgMWo2hhfUdyWMDJtHxAbmORVtBBs1u//2A/7QukxjGmy8NxV9bj/urIx8DGTrI Ts/Q== X-Gm-Message-State: APt69E2WtmZAPoh72uNb5jt6DrHk0aWEQDqlKJbn6yPqHg4fwNFPSASb 2EQYftbATrNBtWsCt/x1+GT/UA== X-Received: by 2002:a2e:330b:: with SMTP id d11-v6mr2747046ljc.67.1529010478380; Thu, 14 Jun 2018 14:07:58 -0700 (PDT) Return-Path: Received: from localhost (109.247.202.84.customer.cdi.no. [84.202.247.109]) by smtp.gmail.com with ESMTPSA id 83-v6sm1117515lje.26.2018.06.14.14.07.57 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Thu, 14 Jun 2018 14:07:57 -0700 (PDT) Date: Thu, 14 Jun 2018 23:07:56 +0200 From: Richard Williamson To: Steve Awodey Cc: Thierry Coquand , Homotopy Theory Subject: Re: [HoTT] Quillen model structure Message-ID: <20180614210756.GC2094@richard.richard> References: <20180614183959.GA1401@richard.richard> <54A8E26C-ECF8-441A-AC3F-7643DA47C3FE@cmu.edu> <20180614201503.GA1968@richard.richard> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <20180614201503.GA1968@richard.richard> User-Agent: Mutt/1.9.5 (2018-04-13) > Exactly. It has been a little while since I was really working on > this stuff, so I could be forgetting something, but as far as I > know the test model structure on cartesian cubical sets is > exactly the one coming from the theorem of Cisinski that Thierry > cites using the obvious cylinder, and with empty S. Now, Thierry > also says, I believe, that this model structure is the same as > the one of Christian Sattler. How can this be?! I was mis-remembering. If one looks at 8.4.34 - 8.4.38 in Les préfaisceaux ..., one sees that S is taken (of course, now that I think properly about it!) to be the (non-empty!) set of horn inclusions. In summary, the difference, from the point of view of Cisinski's theory, between the type-theoretic model structure and the test model structure seems to be precisely the choice of S. Thank you to all!