From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:22f:: with SMTP id 44-v6mr302247plc.42.1528969707097; Thu, 14 Jun 2018 02:48:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:6147:: with SMTP id o7-v6ls1542743pgv.12.gmail; Thu, 14 Jun 2018 02:48:26 -0700 (PDT) X-Received: by 2002:aa7:8253:: with SMTP id e19-v6mr1684816pfn.20.1528969706192; Thu, 14 Jun 2018 02:48:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528969706; cv=none; d=google.com; s=arc-20160816; b=Q1luGDu0iUSvDx7mEnC0U5Bm5DfLBRy4QAg9bD/fY/2MwBaESgWmslw085Hz/tRnJx esqKoix/mUqpQYiCgx7LwIgXE4cz6BTqiT9LwVjzT4tPCPGtYxIgzDKyDBmRM3QMCfX1 0NNSx5/aTEg1etx/LF9xhbGVgOctUu1cQXYQBRXZFYtZF6lsaOiM2R3eJbFq+DV5CqO/ ep1CBHBpXb4XhK0PH/biLOMg8dbJ3l7gdkAmZWRjODRKiuTxbx49zD4Gg5F2mqgoS25R djNGcDLPaQWmIZYAictdGia6QbmQe5p1IM3jV/np6rZQlzcyL3nabQ4M4xN2e1wrznmW QPNQ== 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=TwbW3U41jnu1pkhoHlDQRkrg08rG7n2cWE41kvBAOM8=; b=L6/c5BWqKdE26qro0gvgNZyDGwaHYzyvYRGpS7O0f7fKmPy0kqhrg9Pg7kvRH2OvVH wToVpB8KOTd6KfiHDVzXlifIFlxCBWgD65RiMjy4XXd4/cFk+kfDUXgsOUsCJGP+GoH9 t3EQn5DSKwtw08YqGRwJ3Nq/smaTefgvDi2sL1qOU8+X3r/bWp94CABKXToIFyWIKzqF BNcIFRnIjGI/7q5+3Fs6rvJyqGtxmvx959wzrLcCE17i5mHUYRqv7ySloFxIeqlJhnZW KjBqPqOlZw1QYeYOZV4a2XNjp8eFiAVf1kE4S0WmjSAFDgDKotOEOThN6PkTxE40yTE7 M1fw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jT94UbJ9; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c05::232 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yw0-x232.google.com (mail-yw0-x232.google.com. [2607:f8b0:4002:c05::232]) by gmr-mx.google.com with ESMTPS id b19-v6si277863pls.3.2018.06.14.02.48.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Jun 2018 02:48:26 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c05::232 as permitted sender) client-ip=2607:f8b0:4002:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jT94UbJ9; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c05::232 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-yw0-x232.google.com with SMTP id t198-v6so1919637ywc.3 for ; Thu, 14 Jun 2018 02:48:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=TwbW3U41jnu1pkhoHlDQRkrg08rG7n2cWE41kvBAOM8=; b=jT94UbJ9qG5JlkUwmSvNs4PTZuoq2e3A1wR1KNmI9tOTrmmOV/Sg68/0aFsrGCTpxQ 8ovv2vp6jB50UkBL+NFlWY+Gmn/8pjZ2ENC1tg1DZhszOvnYFKUW9UIsPPHUULXjb4Pp oVRnRPwV/QTom9clgS3mhG9Yq9sJWaVSlkMbbNXba8SQRyM731aRH2/j0phkcp6u4A4w 0X+FT8ao3rRBC6Iqla6TbYNYbqiiK6jhd9eZN7jKBwfucnw66b0v85i1OSdMkdOFg97G pWl7SHuiSWyr1YuEmbi2Y5V1u0qGBOBMyTiC4S9HqgpON1I4L0HClHRDVHAvmV2qNTj3 I/EA== X-Gm-Message-State: APt69E2l8Fx2sx1ummz/LQ1TbsZgAfwKnVWvrhcReBroGBbSsfoiuHQf 8iXukU0ejGYE4nELQsqILooeJYjAN13o6+h8Q4w= X-Received: by 2002:a0d:cbc9:: with SMTP id n192-v6mr928519ywd.399.1528969705347; Thu, 14 Jun 2018 02:48:25 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a0d:c3c6:0:0:0:0:0 with HTTP; Thu, 14 Jun 2018 02:48:04 -0700 (PDT) In-Reply-To: References: <0E61BE7A-910A-4CF4-9A0B-FD05B45EE82A@cmu.edu> From: Bas Spitters Date: Thu, 14 Jun 2018 11:48:04 +0200 Message-ID: Subject: Re: [HoTT] Quillen model structure To: Steve Awodey , nicolas tabareau Cc: Michael Shulman , Thierry Coquand , Homotopy Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable There has been some work by Nicolas Tabareau's group to try and prove the exactness properties. E.g. https://homotopytypetheory.org/2016/01/08/colimits-in-hott/ https://jfr.unibo.it/article/download/6232/6389 and perhaps even later work. It would be interesting if the Cartesian cubes would provide a counterexample to this approach, and show that a 2-level type theory is really needed. On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey wrote: > > >> On Jun 14, 2018, at 12:00 AM, Michael Shulman wrot= e: >> >> In the 1-categorical case, I believe that every locally small >> (co)complete elementary 1-topos is defined over Set: its global >> sections functor has a left adjoint by cocompleteness, and the left >> adjoint is left exact by the Giraud exactness properties (which hold >> for any (co)complete elementary 1-topos). Such a topos can only fail >> to be Grothendieck by lacking a small generating set. > > yes, that=E2=80=99s correct. > >> >> In the oo-case, certainly cartesian cubical sets present a locally >> small (oo,1)-category (any model category does, at least assuming its >> locally small as a 1-category), so it seems to me there are three >> possibilities: >> >> 1. Although they are presumably an "elementary (oo,1)-topos" in the >> finitary sense that provides semantics for HoTT with HITs and >> univalent universes, they might fail to satisfy some of the oo-Giraud >> exactness properties. Presumably they are locally cartesian closed >> and coproducts are disjoint, so it would have to be that not all >> groupoids are effective. > > that=E2=80=99s possible, I suppose =E2=80=A6 > >> >> 2. They might lack a small generating set, i.e. the (oo,1)-category >> might not be locally presentable. Every combinatorial model category >> (i.e. cofibrantly generated model structure on a locally presentable >> 1-category) presents a locally presentable (oo,1)-category, and the >> 1-category of cartesian cubical sets is certainly locally presentable, >> but I suppose it's not obvious whether these weak factorization >> systems are cofibrantly generated. > > but they are cofibrantly generated: > > - the cofibrations can be taken to be all monos (say), which are generate= d by subobjects of cubes as usual, and > > - the trivial cofibrations are generated by certain subobjects U >=E2=80= =94> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I= ) for all A >=E2=80=94> I^n cofibrant and there is some indexing I^n =E2=80= =94> I . In any case, a small set of generating trivial cofibrations. > > > Steve > >> >> 3. They might be a Grothendieck (oo,1)-topos after all. >> >> I don't know which of these is most likely; they all seem strange. >> > >> >> >> >> On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey wrote: >>> 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 wr= ote: >>>> >>>> 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= call >>>>> =E2=80=9Ctype-theoretic=E2=80=9D >>>>> since it is built on ideas coming from type theory), which can be don= e 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 mess= age >>>>> to this list last year >>>>> July 6, 2017 (for another notion of cubical sets however): no quotien= t >>>>> operation is involved >>>>> in contrast with the "small object argument=E2=80=9D. >>>>> This kind of factorisation has been described in a more general frame= work >>>>> 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 th= is 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 interes= ted in >>>>> the more syntactic >>>>> aspects of type theory. It implies that if we extend cartesian cubic= al 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. >>>>> >>>>> 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 arg= ument he >>>>> presented last week at the HIM >>>>> meeting. Ulrik Buchholtz has (independently) >>>>> more abstract proofs of similar results (not for cartesian cubical se= ts >>>>> however), which should bring >>>>> further lights on this question. >>>>> >>>>> Note that this implies that the canonical map Cartesian cubes -> De= dekind >>>>> cubes (corresponding >>>>> to distributive lattices) is also not a Quillen equivalence (for thei= r >>>>> respective type theoretic model >>>>> structures). Hence, as noted by Steve, this implies that the model st= ructure >>>>> 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 discus= sions >>>>> about this last week in Bonn. >>>>> >>>>> -- >>>>> You received this message because you are subscribed to the Google Gr= oups >>>>> "Homotopy Type Theory" group. >>>>> To unsubscribe from this group and stop receiving emails from it, sen= d an >>>>> email to HomotopyTypeThe...@googlegroups.com. >>>>> For more options, visit https://groups.google.com/d/optout. >>>> >>>> -- >>>> You received this message because you are subscribed to the Google Gro= ups "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. >>> > > -- > 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.