From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.65.70 with SMTP id f6mr8845506ywk.9.1501363185923; Sat, 29 Jul 2017 14:19:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.30.16 with SMTP id e16ls5054521ioe.46.gmail; Sat, 29 Jul 2017 14:19:45 -0700 (PDT) X-Received: by 10.129.52.87 with SMTP id b84mr8653855ywa.226.1501363185201; Sat, 29 Jul 2017 14:19:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501363185; cv=none; d=google.com; s=arc-20160816; b=bH+aYD5PWZnuzWfXrkTvTsM9i9CZsO/HfG9O3oHv7cNubp5UXOJsVClN7uNpQ7or/s j07ZGiI754OcNCIgzfAfQfw+LFcn1SS3SLZZREXG2qptAifqFiZ1eOyCZvv9u1bkNF7n oosl6Hz1TdPnLvwk5VHeCdbePjPmuOGYkRYZberuxR3YaD2X8ZQWwYnSK56IM04k23ff qXe+TN9ICfTOgEfX+XV6hJn76cIjRi9wA/ZwkZpeNeKgehAeBYjIS2Lb3yI+YiD/QgSD C1azadkT1e4tcamKiND5PTWrn2ht10rlmDsnWdH8dMffJPElOKDn1gRkFT4U7MnpUkzv 6cBQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=nkYTDnmvWaoFFoW/6Kl4Y28H1UIb/O9Ha/i47ZzBPxY=; b=qIkdP8Ve8Y0vt6zlTx3swW5ZZtfGopm0avAGwiqYq+X+7SaTIvuctB0bc7qjwXF+Dg Vi0jhMm74lW3S5RG1wRYbDpwBRpz9VRyS/cRKgPoSyvHA9wYZBt79KJJ2cRtZFt7wMK7 LLv+wQbPJLtxihHyy1cXPfn2iRFGs/8aOm8TK40G+bfU9PG/K+0wzf+EmY8qu+DUoz9B /uw+Jx2/fo+auhaEi91I+flFH023pSA6Jr0X1wUI+B1oltiKCCrDwUPIhP49/XigYT1w WGLFABTm0UgJuyf/HenFf7JXOcj0OqDrCkltMPFw6afpYcETj8kQ3m3UeGRh8JEGJW1y Hsyg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=mF1yuT8p; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x232.google.com (mail-yw0-x232.google.com. [2607:f8b0:4002:c05::232]) by gmr-mx.google.com with ESMTPS id h5si1474195ywd.12.2017.07.29.14.19.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 29 Jul 2017 14:19:45 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=mF1yuT8p; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x232.google.com with SMTP id u207so78257002ywc.3 for ; Sat, 29 Jul 2017 14:19:45 -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; bh=nkYTDnmvWaoFFoW/6Kl4Y28H1UIb/O9Ha/i47ZzBPxY=; b=mF1yuT8pPA/KZjuFs60Y+rxFZvpsP3A2jh+i70By6KzcDpA9r/sUSA1+LF8wN/3qio GAJhsQ4MRQ1oDTdJLV17zMqqtQN8U+lbd3lmWkFxlBBaDC1X1L3n5icb5kYlUIdLmCMG /x8fxDah6OVJUAtSRnUmH9aVInl+pwoNHGRoY9VEJnBe6u8EtE0Z0mMteQPAlPpcvvM7 zKpmY8xOD9ZWSAuVBHh4Xms2INnTvcw/WnizAolUqDEREzbjB7jKMA1QSPSu+Jr3j4jO Xcqz82gtl639X7wzRCSULYz0aZ2XhEVEclvrbps7nOxU9hGR7NSJk7eBWk90vjZbOIJA 4kYg== X-Gm-Message-State: AIVw113ZuAuIVw2ktQnbQw8Zt8LyDBTaqCL3E+PT3UVYGp/SscywvH9Y yakZ8YdnqMtlr/Gs/8M= X-Received: by 10.13.231.67 with SMTP id q64mr10640572ywe.71.1501363184617; Sat, 29 Jul 2017 14:19:44 -0700 (PDT) Return-Path: Received: from mail-yw0-f179.google.com (mail-yw0-f179.google.com. [209.85.161.179]) by smtp.gmail.com with ESMTPSA id p127sm9129776ywf.46.2017.07.29.14.19.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 29 Jul 2017 14:19:44 -0700 (PDT) Received: by mail-yw0-f179.google.com with SMTP id l82so81374281ywc.2 for ; Sat, 29 Jul 2017 14:19:44 -0700 (PDT) X-Received: by 10.13.219.79 with SMTP id d76mr10766443ywe.79.1501363183892; Sat, 29 Jul 2017 14:19:43 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Sat, 29 Jul 2017 14:19:23 -0700 (PDT) In-Reply-To: References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> From: Michael Shulman Date: Sat, 29 Jul 2017 14:19:23 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: cubical type theory with UIP To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" But it seems to me that cubical type theory could solve these problems in a nicer way, which is why I asked. On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri wrote: > Now I'm having second thoughts. Quotienting together hprops might make type > equality computationally relevant. Not something you want with OTT's strict > props or ETT's equality. Maybe 2-dimensional type theory would be good for > the job. In this case the 2-cells would not be distinguishable by equality, > but might still have computational content. > > > On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: >> >> Sorry. I got distracted because the type theory you seem to be asking for >> doesn't sound cubical. Like I said, I suspect OTT could handle hprop >> extensionality, if it doesn't already. Probably ETT could too. >> >> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: >>> >>> As I said, >>> >>> > The motivation would be to have a type theory with canonicity for >>> > 1-categorical semantics >>> >>> So no, I don't want "the model" to be using cubical sets, I want >>> models in all suitable 1-categories (e.g. Pi-pretopos etc.). >>> >>> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri wrote: >>> > Only up to homotopy? So you still want the model to be using cubical >>> > sets? >>> > Actually, couldn't you interpret OTT into the hsets, internally to >>> > HoTT? >>> > It'd be a hassle without a real solution to the infinite coherence >>> > problem, >>> > but it should work, since the h-levels involved are bounded. >>> > >>> > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >>> >> >>> >> Right: up to homotopy, all cubes would be equivalent to points (hence >>> >> my question #1). >>> >> >>> >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri >>> >> wrote: >>> >> > I'm confused. So you want a cubical type theory with only hsets? In >>> >> > what >>> >> > sense would there be cubes, other than just points? I thoght OTT had >>> >> > propositional extensionality. Though maybe that's only for strict >>> >> > props. >>> >> > >>> >> > >>> >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >>> >> >> >>> >> >> I am wondering about versions of cubical type theory with UIP. The >>> >> >> motivation would be to have a type theory with canonicity for >>> >> >> 1-categorical semantics that can prove both function extensionality >>> >> >> and propositional univalence. (I am aware of Observational Type >>> >> >> Theory, which I believe has UIP and proves function extensionality, >>> >> >> but I don't think it proves propositional univalence -- although I >>> >> >> would be happy to be wrong about that.) >>> >> >> >>> >> >> Presumably we obtain a cubical type theory that's compatible with >>> >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a >>> >> >> single universe of propositions. But I wonder about some possible >>> >> >> refinements, such as: >>> >> >> >>> >> >> 1. In this case do we still need *all* the Kan composition and >>> >> >> gluing >>> >> >> operations? If all types are hsets then it seems like it ought to >>> >> >> be >>> >> >> unnecessary to have these operations at all higher dimensions. >>> >> >> >>> >> >> 2. Can it be enhanced to make UIP provable, such as by adding a >>> >> >> computing K eliminator? >>> >> >> >>> >> >> Mike > > -- > 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.