From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.60.45 with SMTP id q42mr856299otc.117.1496328230196; Thu, 01 Jun 2017 07:43:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.5.5 with SMTP id 5ls2736436otw.11.gmail; Thu, 01 Jun 2017 07:43:49 -0700 (PDT) X-Received: by 10.157.33.117 with SMTP id l50mr857873otd.64.1496328229482; Thu, 01 Jun 2017 07:43:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496328229; cv=none; d=google.com; s=arc-20160816; b=W7tAiPRecP9+7ChYnQHBEpm4qeqBRJOKvy7cH7uqD+uBEXTWsGvq8dMOh3yfU3017U 6cEBlej1TM0H+eDuMmsGmrcybirSlsq9AwNrQkK1YoEQ9Bqw44RjEUA56V42qaBgoKtm z1BOjk7e3yO0iUCpsp+8p0ONrXu9RCXlv852LozOuJ20k8+G7r/LbJ1Rv+Kg0PVHgrNj j1/X3N9TQYGQMos2MOOUPdAp9pE/iFXB4gPPfeUlDHWbJJEkCyJhedE9WO8uxeT03+0e lI2lg7B5wsJcNfH3Lt0VfIsMEoT3fq/uYVTY+jrFqICuz7QK7WSAutk3lrLp4bWzEsSB fbPg== 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=ZWLf+vra3op1MthxzzkomrhbLWbF2CyTsE4x9anTqdI=; b=jWsoCvZi+pncyAr3usCG3LN0AYvEGh201xFnbtVx/upLOU/S1WHPWX23BQN+G03Ojj TQEp3f54pcKdKTuyBhnpJUnxJeW7jmIdwzWpGk9d0rd1TEx5aIvEbNA+LXBu1OncFh2C vbdaB7Qu1aN1e2Ro8wDc6v5sQYnU5/KWULLCWeoZuKUriTAccaK1ThYqORNRsjF3+aNk uhHmfoaRcC0X3+t/ZAoyXrpjumRGUYEnmM5beFa9z841csYXnsnOomZDrLSkXJC/vKmd 1oG8FViSXmxEAYI3uqfgkmrmumj0vfe+zbMpADUFPapuLRevBfkJZB8znshiNMuRcZ1A /xUg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x234.google.com (mail-yb0-x234.google.com. [2607:f8b0:4002:c09::234]) by gmr-mx.google.com with ESMTPS id x190si1161720ywg.13.2017.06.01.07.43.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 07:43:49 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x234.google.com with SMTP id 202so11314931ybd.0 for ; Thu, 01 Jun 2017 07:43:49 -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=ZWLf+vra3op1MthxzzkomrhbLWbF2CyTsE4x9anTqdI=; b=gWIg1a5TXG4NdcyrkLQnwP3ffnecGYpuyW3t6zD3Iagddl+wFueMXpibZeyg3Stq/M 8ho0iHFKNDUWCDMz4M1XnislcrUL6uuq1E10N8DhMMSCjFKc99Bd5p/GbrrU+rAYtJ+p CSm29aGUUfd2ySX9FmfXDtKRAz0mHvbgzXijwnW0c8HF1WudgLx/SRGtxfbP40IwHy3g 4FTl5O4Vz/BcyYGyOmmj8GaOKbYsOIP47uN5+iSIdL+dYE/3bWCymu/pm+mM0J1EoVac g7X700tcq9Dsrbrnv9VwSE776aWYKIBD2lvFCrFTsgcoDvj3Eb0CqNhl6idDwIBfJFxc umKw== X-Gm-Message-State: AODbwcAmZwCsg9Zsq4elLMRF+RWvY85FHw8TR7pMd/Zkbi5CjjaJbtMg 5f330XYS9lWX02zQYpw= X-Received: by 10.37.113.84 with SMTP id m81mr28692843ybc.70.1496328228939; Thu, 01 Jun 2017 07:43:48 -0700 (PDT) Return-Path: Received: from mail-yw0-f169.google.com (mail-yw0-f169.google.com. [209.85.161.169]) by smtp.gmail.com with ESMTPSA id z194sm9311915ywa.24.2017.06.01.07.43.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 07:43:48 -0700 (PDT) Received: by mail-yw0-f169.google.com with SMTP id l74so21006524ywe.2 for ; Thu, 01 Jun 2017 07:43:48 -0700 (PDT) X-Received: by 10.129.77.85 with SMTP id a82mr1452606ywb.266.1496328227714; Thu, 01 Jun 2017 07:43:47 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.18.215 with HTTP; Thu, 1 Jun 2017 07:43:27 -0700 (PDT) In-Reply-To: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> From: Michael Shulman Date: Thu, 1 Jun 2017 07:43:27 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Semantics of higher inductive types To: Thierry Coquand Cc: homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Yes, this is something rather mysterious to me. There may be something special about the cubical model that enables a sort of "horizontal/vertical" decomposition of fibrations. Peter and I thought for a little while about whether there is some similar sort of "fiberwise fibrant replacement" that would work in a general model, but weren't able to come up with anything; however, perhaps we just weren't clever enough. I do think it is very important not to be limited to one particular model. On Thu, Jun 1, 2017 at 7: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. > > 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.