From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.4.21 with SMTP id 21mr18549585otc.44.1495736781243; Thu, 25 May 2017 11:26:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.68.164 with SMTP id v36ls1250418ote.28.gmail; Thu, 25 May 2017 11:26:20 -0700 (PDT) X-Received: by 10.129.77.66 with SMTP id a63mr19719789ywb.8.1495736780810; Thu, 25 May 2017 11:26:20 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1495736780; cv=none; d=google.com; s=arc-20160816; b=dU9fv2EkZGj8tTWd71H1E+xDGTASbFzK1BSGjkh3NwU7FPCT4J0MeQqsNzyQ7493rj Wxczo+zOnLETG7aWFxmMdKasmyl9LuA8BrYhX6mzfT5bFMr3m+D9ndTzVGLudu9Vv/L0 tWfJiUMWzjE4HZPBBKSrD58r1AGHaoPB5L91RX7Lo0Eol92oDYc8JFuNqNpEcDftJrPc gJXpU9Spk6QmRZC9LJsRjtXbpVmAPbM9RS8MDg8r1szIAokuscFD+rE32CCIrJUMIBTE bt3iLhE4AtHhtZd/3hPYy5ineOtNDTq36WGcBKfAM3A0a8kJIcINCqAVKf3ITqhMhZT6 32vA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature:arc-authentication-results; bh=vWw7MmYoj/U7TAwThFjMTj6u8AFaqIHSJj0ro9vxKZs=; b=VHpM0I57An2O0uVY2/4G010eOs2kzFIUNno6heRon6tgibQhd2vRXK40xZNACIWDQf i818eh2+/frDSwq4iq0iUX7rfDU/IYWiDg2aVDURK9K0RoXmMICZAUk4JBLNeNC+Vvcj Tokjz+5y3gXIhmJVHQh3jNAzS62Apk3oy35u939nNh9d5w1Qf69l2H3++XTZmJAu9RHJ PlqPFA3lFbZEKfFMbC7Y7ds2Cbf5uyL9PcYOQeU0zKevXOo+mC+4q8+PY0rz8Tn52Ptd dOi5J3hNcmxOCVwGj8vgfvP7b16Al15T8jz3paltMufkM5X9jSePYnkhA7xx+Ij/PHLz zXGw== 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::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x22d.google.com (mail-yw0-x22d.google.com. [2607:f8b0:4002:c05::22d]) by gmr-mx.google.com with ESMTPS id o66si1051883ywd.7.2017.05.25.11.26.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 May 2017 11:26:20 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22d.google.com with SMTP id b68so107202270ywe.3 for ; Thu, 25 May 2017 11:26:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=vWw7MmYoj/U7TAwThFjMTj6u8AFaqIHSJj0ro9vxKZs=; b=yANwAHBRkpVXWU1P+u9gpUhnIc5/nN93wPjkrhrrWwYRlKM3XA+tu1AXnG9wnsqcxE m9tYqDwPOmjXT/+fd5c9b90hZzBTO6BLAQoGP83Q5v+92YJHFRAHMezcPhKpoX4KQv3U FcRSZvpbMFj8wv/JLAdtUjSicGjNijD+91y/wE6C8BiWVQnXWfNcMu8TOTdAb/y895r/ +Omzr7k8xz1DzJjpDHBloLYm+wuvQL4H25niN8zSa906pN1X68Ll/A0f98gmgNFwG/Gf 41Vh/fCvJ/uHs+riMmCyW2BiqV0EP8KLsH5Lv4cNV8/fVfy6hbgcnynhm09zKtRVfYvc GKoA== X-Gm-Message-State: AODbwcB4w0GZJjPDjnedGDjdc9lYt7uoETPGjTFPvIZtwzidipA8yIGN RjTwe+c6mjQFQYuqjIU= X-Received: by 10.129.178.68 with SMTP id q65mr11438745ywh.31.1495736780358; Thu, 25 May 2017 11:26:20 -0700 (PDT) Return-Path: Received: from mail-yb0-f170.google.com (mail-yb0-f170.google.com. [209.85.213.170]) by smtp.gmail.com with ESMTPSA id e67sm4404796ywa.62.2017.05.25.11.26.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 May 2017 11:26:19 -0700 (PDT) Received: by mail-yb0-f170.google.com with SMTP id p143so54527237yba.2 for ; Thu, 25 May 2017 11:26:19 -0700 (PDT) X-Received: by 10.37.174.32 with SMTP id a32mr17522471ybj.50.1495736779612; Thu, 25 May 2017 11:26:19 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Thu, 25 May 2017 11:25:59 -0700 (PDT) From: Michael Shulman Date: Thu, 25 May 2017 11:25:59 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Semantics of higher inductive types To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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.