From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:6bc2:: with SMTP id m2-v6mr1315737plt.21.1518019641390; Wed, 07 Feb 2018 08:07:21 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.153.155 with SMTP id t27ls660253pfk.11.gmail; Wed, 07 Feb 2018 08:07:20 -0800 (PST) X-Received: by 10.99.51.2 with SMTP id z2mr1188500pgz.152.1518019640171; Wed, 07 Feb 2018 08:07:20 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1518019640; cv=none; d=google.com; s=arc-20160816; b=XsE3BXZmd6jXRnmgiplcqzHhOwjutj9SAzggY4rhoLVNxy/hU4fDwmbZIdwmaERCMA 7n0hKX5TvlZY4ht4KDVU7D/elbJYhx8Xq0N6IPlJC24oDDps9fpMGG8W+/RfL1qRggJw fsJgITe/qzMOW+wOaapFOaKfgdPBFZ14QwonQoFnRYKeH60v3Z7qtBoY66LnGUpF46SO iVaV3U+8UEH5snNJcNq/P7XgkxbRgSlBwQdoxoPzSvpfuZeFIElwXwfLdKu7Tu2ypkfP 4W16QzMF6yF2Rjj/vLl0CZ8YY2AgGDNRP3CEHOsiUYhj+oTYUNxeep1IwuYWNvUfM8GC 14qw== 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 :mime-version:dkim-signature:arc-authentication-results; bh=Q8S8V2GysEATprpLegZt5QQ5YiF633UCGDk4p7mCtQg=; b=zfLDmO4ZeDvLy0C1r472DQAMjAE9ki2vXUr4JNzaZHXQWhQrBv3Yr/KqSfTHwOHZ7Q k5O9abvnwbehXucojTSxHzH2pfpSzFhBDBn+Jo595ab82tetwWFnos1po0/6YryurcZM UlxmLUyvQpkNZwkoZG5JirrVyFlLFMRq0G8dQo2bARsfqLMSqmB7GDv0N/UBVKr/YiGF +W5dV4uCaEdhVnBumYXWJVKiK53aEINEanb8U0zjNqazDU8ZFaHSnPd4fyonPX+msWdh gEQ76GEhFKodzQSXN8eviDNvxVg1+DCFbFnc+HA0c+S6DMGxVG3rKP5Zh4KY+tx+NAXe sZzA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=q8XhspN/; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::22f as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk0-x22f.google.com (mail-qk0-x22f.google.com. [2607:f8b0:400d:c09::22f]) by gmr-mx.google.com with ESMTPS id o135si95686pfg.5.2018.02.07.08.07.20 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Feb 2018 08:07:20 -0800 (PST) Received-SPF: pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::22f as permitted sender) client-ip=2607:f8b0:400d:c09::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=q8XhspN/; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::22f as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qk0-x22f.google.com with SMTP id m130so1737891qke.1; Wed, 07 Feb 2018 08:07:20 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:cc :content-transfer-encoding; bh=Q8S8V2GysEATprpLegZt5QQ5YiF633UCGDk4p7mCtQg=; b=q8XhspN/BC2l61adt65JxDQo5rnY9Q9bcJv7OfuObh3L0oXz61DTHswgzG5qnZ97dS j53aL0dJhMbco6wOg4rrWpbLg7I6pAj0vUo8hgEddXo1dhw81Vkp8e4H2AKbuNNxkF21 M6KaEpxxsRbkwF1GYD8SsssIyZv4tUytqW4MUeWCz6Q1+TSscI6S6wOTe+IWkL0/XUNP w0gVwDHQW96NEsH+Jfh7u4z7Lf3pG4HLM1xKaaUtF0aZ4Nl7ZPNlJPWpDzWfIwEItmq7 qm4u2r4uXFrlCzUghdiOWFNHCcPiNbKbZgTAWiOm9Ee2k6/lu0a4UcGJ1PLBSIKX4MC2 gwMA== X-Gm-Message-State: APf1xPCMvFCPr7kNERYvAsyAHgEca18Ky1UIuaWC87OdSfJV0g6pfRDR 7sBzY7Oe5fw6jVzMiBt9uBqZS/bwyK5UCGkNdIjYGg== X-Received: by 10.55.116.68 with SMTP id p65mr10133712qkc.230.1518019639193; Wed, 07 Feb 2018 08:07:19 -0800 (PST) MIME-Version: 1.0 Received: by 10.140.82.8 with HTTP; Wed, 7 Feb 2018 08:07:18 -0800 (PST) From: Anders Mortberg Date: Wed, 7 Feb 2018 11:07:18 -0500 Message-ID: Subject: On Higher Inductive Types in Cubical Type Theory To: Homotopy Type Theory Cc: Univalent Mathematics Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We recently uploaded the paper "On Higher Inductive Types in Cubical Type Theory" to the arxiv: https://arxiv.org/abs/1802.01170 ----- On Higher Inductive Types in Cubical Type Theory Authors: Thierry Coquand, Simon Huber and Anders M=C3=B6rtberg Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers. -- Anders, Simon and Thierry