From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.0.150 with SMTP id 144mr804182pfa.36.1496331558108; Thu, 01 Jun 2017 08:39:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.31.136 with SMTP id d130ls440385itd.15.gmail; Thu, 01 Jun 2017 08:39:16 -0700 (PDT) X-Received: by 10.99.142.68 with SMTP id k65mr966147pge.85.1496331556864; Thu, 01 Jun 2017 08:39:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496331556; cv=none; d=google.com; s=arc-20160816; b=P9D28XmBoKDkP9kd650bYMjRVaS7gGXpqBweZ9P5+crMmy+Sp+S2kOaH/ghrRxZAzm nUGtUyKRNruS0AeIFqp5CIBS26GjoctCg7eFKZZ33DUnyaotDTq+dtRK6h01sjFmd2R5 vSVK1SmuH9H7Qenuxuh/GiRYiolOGeiOfRay+Lq2HT58kTnuIeSdN7+4/LJhNmkyEV2r kaSbHHxReal+cMOAWYiTH6dSFLQhKBL2644ToABY3lMw7bQ0XFnuOsjYWEuBaMTalzsq 6+9+anrTmkccIrTpJTeQQ6uqIoioz6LpK991YlRNSUSSUyhsyjjX/VZ62aqRHRPLBoeE h9RA== 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=1kQSUjsad1GLOOlWQEjIRocX3C9k8agDYV/DZmM7Q+o=; b=UsW0g1KqHgjhk124QMAyCb/9NVRWYHrELbNWkdNf3U+1qhnyr/28GE0Rcac4L27jNY +7vrYmoUou185dQufnbxP/xj9mZVeGVWpdwPD8RvA/8hvk3AEadtl7ROXET3k87UuFFY UvlveBlKlf2qw+z5pE/I+yfPe4GY5Pq4TYHwl4kdCu4CYIRAGoknchqrQeFcwTmH0K/5 PPgbxhyTpnDVC/3cYthfnI5qUaK8B5L85dGYQLxyEftQ90EO2xDW7WjHhvZb9eLMPkwG hub7ewj3xsMozBbxgz6dqC3BXSCHBMRvHXeHxqS1RbgnTka3NO6m9DbgqLNW0EgrBM2A kbXQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::242 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x242.google.com (mail-yw0-x242.google.com. [2607:f8b0:4002:c05::242]) by gmr-mx.google.com with ESMTPS id p205si1038870ywg.4.2017.06.01.08.39.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 08:39:16 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::242 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::242; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::242 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x242.google.com with SMTP id h82so3004094ywb.3 for ; Thu, 01 Jun 2017 08:39: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=1kQSUjsad1GLOOlWQEjIRocX3C9k8agDYV/DZmM7Q+o=; b=WPYW6NJRjCb4JJw4zTBTicM7Ll7txFGdfSdIG3ZJ+upbeQROcgIJTSKzz+rcHzzawW m144vjZZCJqtXlgIGkd8Wuoo2yQtDuEq2QQRitAYxmAm4GTKR/vQIM3deRo7BYvS224P YRc4wloKrET6Q+bJjLUjeTMGrOcIKyjMJt/2g3+Y7gDC+xYCHEPS9bfRPNNELbtIqApB OQcq127MJ3FYlKeA30xlHex8D5+TJOCTPKQg8+DvBf9jlOwqEa+XWUrOZQ2CfBYrleZp NRqMaCxl7bFPdDYJQ7s0u0jCWvKnamU4YF8tpp6P5+F6PN94KUU+s/EpPGCltkg2LXep b9oQ== X-Gm-Message-State: AODbwcBGDYKjCsFu/fo3Ln/MsKcRxkxTfzZ6X3mTift7Tl9nD2QTwya1 Uy+VFwBBGYTO/I2wQ3g= X-Received: by 10.129.89.85 with SMTP id n82mr1730424ywb.94.1496331556217; Thu, 01 Jun 2017 08:39:16 -0700 (PDT) Return-Path: Received: from mail-yw0-f173.google.com (mail-yw0-f173.google.com. [209.85.161.173]) by smtp.gmail.com with ESMTPSA id u187sm9130967ywd.22.2017.06.01.08.39.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 08:39:15 -0700 (PDT) Received: by mail-yw0-f173.google.com with SMTP id b68so21718094ywe.3 for ; Thu, 01 Jun 2017 08:39:15 -0700 (PDT) X-Received: by 10.13.202.87 with SMTP id m84mr1681421ywd.282.1496331555162; Thu, 01 Jun 2017 08:39:15 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.18.215 with HTTP; Thu, 1 Jun 2017 08:38:54 -0700 (PDT) In-Reply-To: <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> From: Michael Shulman Date: Thu, 1 Jun 2017 08:38:54 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Semantics of higher inductive types To: Steve Awodey Cc: Thierry Coquand , homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. (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.) On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey wrote: > > On Jun 1, 2017, at 10:23 AM, Thierry Coquand > wrote: > > 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. > > > 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 lots= of nice properties > for models of HoTT > =E2=80=94 but there was never really a question of the consistency or coh= erence of > simple HITs like propositional truncation or suspension. > > the advance in the L-S paper is to give a general scheme for defining HIT= s > 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. > > Steve > > > 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 c= an > directly > be transformed to a semantical interpretation, as explained in the follow= ing > 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 in > the note > what is the problem solved by the =E2=80=9Cflattening boxes=E2=80=9D meth= od. > > 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 H= oTT > book. > > On 25 May 2017, at 20:25, Michael Shulman wrote: > > The following long-awaited paper is now available: > > Semantics of higher inductive types > Peter LeFanu Lumsdaine, Mike Shulman > https://arxiv.org/abs/1705.07088 > > From the abstract: > > 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. > > 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. > > -- > 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. > > > > -- > 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. > > > -- > 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.