From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.100.23 with SMTP id y23mr831884pfb.23.1496332587475; Thu, 01 Jun 2017 08:56:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.31.39 with SMTP id x36ls5657239otd.25.gmail; Thu, 01 Jun 2017 08:56:26 -0700 (PDT) X-Received: by 10.157.31.52 with SMTP id x49mr998288otd.75.1496332586834; Thu, 01 Jun 2017 08:56:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496332586; cv=none; d=google.com; s=arc-20160816; b=bDohIgR7Qq9SXfPpFjqtLqGWqSCdMo7Xkcwt3v5a8PWZU7UMNbF8xIPN1grvc1LM5O p3hC3r5YTUqKwIAaqvrgxcNSqSrk7H52LsWRKqPmh+vSqutd3vTatgZlUTilh15hb0Vi uyRXWEnS/nzmJ/TjafZflwDFLnexxv1hdSPSrZRs/7BYWWo4vL7sCRDXLfxV4YtsJZvZ l5LPWz+Thyrf1zL1xjyp5JnrwchCS7uK+CtOuQ9OXMYnkejcZlMTdBPSJrZwZSoHI+oJ XWmBdV2eXPIg2zbA2Lv2dd9Z7exxdYS8MeqAk9+hG5p0vwok2pzg95YW/kLyAJ2tpqlF UvRw== 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=0sxcnXS4Sgl8HCOZ1yajZ4SGerQBjN0xtYBgBSNIo/A=; b=obDdHVKZvkqCcwQnxepDsR8oiWDnPB4O93l/hqzUyhekxaq57WEVnBkb8oUwVtrFeu PvY5/2wzfuVHkv8X3cbbA/OLc+n0RkdExTxlupgJgHo9P97bZh+y2COYjIbkXsMT0A6K C1GgclZHLkZoVaBBigUnQVj789DStlJ47F/UDEgLdcteHX2wTbrLZGkrySrC0G2xrj3T K7m2R/LKz3hwjUpnpFglGtKlLTmZZOWcZJmGiV2cYMaXIoRYMuhx2phK5G2xZTbAov3n nb9b+rzfB9Gmr2EoHtLL8j+1EfrVPcR899vfqHqpIHPSXW8sn92VyfY0v8I/MqEfzG2k aBgA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c09::232 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qk0-x232.google.com (mail-qk0-x232.google.com. [2607:f8b0:400d:c09::232]) by gmr-mx.google.com with ESMTPS id m5si1108699ywd.8.2017.06.01.08.56.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 08:56:26 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c09::232 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) client-ip=2607:f8b0:400d:c09::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c09::232 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qk0-x232.google.com with SMTP id p66so23221623qkf.3 for ; Thu, 01 Jun 2017 08:56: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=0sxcnXS4Sgl8HCOZ1yajZ4SGerQBjN0xtYBgBSNIo/A=; b=v0K09eQxaurDo0wVaSPFU586Q+EWwpvgogUABu11pBjNq4qPQn1cxD1TBwkmoKcRc7 yAJLBQWzNRhqrsuvQFnS+hmlo+TIsEkqycdhHu0IjM9bq9yVNinHPgLZVwj0hFMtO2mY 8JiTcJnbq6Up0z16yEhWyCtCyAKFf2Z0KQl/1Suaiix5IavRZcIwIUbUyrn8EQ4WM6y1 F+nfifGsIQn3NL4GBvIe7dUoe9WadNWvcjtZ6JHu/XdAsS3rE0H/vYqGgdIEtLFkhhe9 rtNY/nHtRqfHsbEGxnqr1QIpX/1CdLC5NJc3t4BUiyv76znzREj+7ggQM9M+bnKtqGqX ZSwQ== X-Gm-Message-State: AKS2vOw2z2FqEjJnk3RGxLn8rkqryzEwol9G9eOwaM98j8jA5rkeHzq9 QwHKK0ZNFASOereB X-Received: by 10.55.106.199 with SMTP id f190mr2756682qkc.117.1496332586457; Thu, 01 Jun 2017 08:56:26 -0700 (PDT) Return-Path: Received: from steveawodeysair.home (pool-98-111-244-8.pitbpa.ftas.verizon.net. [98.111.244.8]) by smtp.gmail.com with ESMTPSA id c21sm13170020qtd.60.2017.06.01.08.56.25 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 01 Jun 2017 08:56:25 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] Semantics of higher inductive types From: Steve Awodey In-Reply-To: Date: Thu, 1 Jun 2017 11:56:24 -0400 Cc: Thierry Coquand , homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> To: Michael Shulman X-Mailer: Apple Mail (2.2104) you mean the propositional truncation or suspension operations might lead t= o cardinals outside of a Grothendieck Universe? > On Jun 1, 2017, at 11:38 AM, Michael Shulman wrote: >=20 > Do we actually know that the Kan simplicial set model has a *universe > closed under* even simple HITs? It's not trivial because this would > mean we could (say) propositionally truncate or suspend the generic > small Kan fibration and get another *small* Kan fibration, whereas the > base of these fibrations is not small, and fibrant replacement doesn't > in general preserve smallness of fibrations with large base spaces. >=20 > (Also, the current L-S paper doesn't quite give a general syntactic > scheme, only a general semantic framework with suggestive implications > for the corresponding syntax.) >=20 >=20 >=20 > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey wrote: >>=20 >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand >> wrote: >>=20 >> If we are only interested in providing one -particular- model of HITs, >> the paper >> on cubical type theory describes a way to interpret HIT together with= a >> univalent >> universe which is stable by HIT operations. This gives in particular the >> consistency >> and the proof theoretic power of this extension of type theory. >>=20 >>=20 >> but the Kan simplicial set model already does this =E2=80=94 right? >> don=E2=80=99t get me wrong =E2=80=94 I love the cubes, and they have lot= s of nice properties >> for models of HoTT >> =E2=80=94 but there was never really a question of the consistency or co= herence of >> simple HITs like propositional truncation or suspension. >>=20 >> the advance in the L-S paper is to give a general scheme for defining HI= Ts >> syntactically >> (a definition, if you like, of what a HIT is, rather than a family of >> examples), >> and then a general description of the semantics of these, >> in a range of models of the basic theory. >>=20 >> Steve >>=20 >>=20 >> The approach uses an operation of =E2=80=9Cflattening an open box=E2= =80=9D, which solves >> in >> this case the issue of interpreting HIT with parameters (such as >> propositional >> truncation or suspension) without any coherence issue. >> Since the syntax used in this paper is so close to the semantics, we >> limited >> ourselves to a syntactical presentation of this interpretation. But it = can >> directly >> be transformed to a semantical interpretation, as explained in the follo= wing >> note >> (which also incorporates a nice simplification of the operation of >> flattering >> an open box noticed by my coauthors). I also try to make more explicit i= n >> the note >> what is the problem solved by the =E2=80=9Cflattening boxes=E2=80=9D met= hod. >>=20 >> Only the cases of the spheres and propositional truncation are described= , >> but one >> would expect the method to generalise to other HITs covered e.g. in the = HoTT >> book. >>=20 >> On 25 May 2017, at 20:25, Michael Shulman wrote: >>=20 >> The following long-awaited paper is now available: >>=20 >> Semantics of higher inductive types >> Peter LeFanu Lumsdaine, Mike Shulman >> https://arxiv.org/abs/1705.07088 >>=20 >> From the abstract: >>=20 >> We introduce the notion of *cell monad with parameters*: a >> semantically-defined scheme for specifying homotopically well-behaved >> notions of structure. We then show that any suitable model category >> has *weakly stable typal initial algebras* for any cell monad with >> parameters. When combined with the local universes construction to >> obtain strict stability, this specializes to give models of specific >> higher inductive types, including spheres, the torus, pushout types, >> truncations, the James construction, and general localisations. >>=20 >> Our results apply in any sufficiently nice Quillen model category, >> including any right proper simplicial Cisinski model category (such as >> simplicial sets) and any locally presentable locally cartesian closed >> category (such as sets) with its trivial model structure. In >> particular, any locally presentable locally cartesian closed >> (=E2=88=9E,1)-category is presented by some model category to which our >> results apply. >>=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 >>=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 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.