From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.135.50 with SMTP id a47mr1322737wra.12.1501666820284; Wed, 02 Aug 2017 02:40:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.169.130 with SMTP id s124ls466816lfe.36.gmail; Wed, 02 Aug 2017 02:40:18 -0700 (PDT) X-Received: by 10.25.125.67 with SMTP id y64mr2369930lfc.42.1501666818242; Wed, 02 Aug 2017 02:40:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501666818; cv=none; d=google.com; s=arc-20160816; b=IqQ82nCYCMB4i3V1ZrqJ4WY3ouk0qG0K2yUfKnmhyLyZwkpDvNGxe+otbQHUm+yMbm mG0RQr+2z5/bjsjGcrol9ngx6WtzXQxd9GbUH+T/sGfQlR/4RAJ9n6as7oK3qEszKLN7 tF5CfMQ8H3CxZs/SzirdHos1zoO1LlEnCiBta7OpvHN9H/qDBhlxYvreyakTSiS/UCzr PFzGO0HUfJ4mH+Vf0AhC4JGfdkRS7WurruXda/xnjw5OAFxRGCIgakvQcCDz32vYOHop 9JErRIYnH9DXCbpgx+e7lThSBBj3aiO85mFH+slj7XdbXlercEKcpbpzOu1n5Mdd/12w 7Kkw== 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=FrdwwPzas7zeFcUiHay9mFBT+gXEFy8NJKgdebodWlU=; b=zHRVyxQsD7EWmQaf/xSBP+jeFYp9ih/u2sOP5iV1ZOUBIpr6J4qZ7GOoYPGCOZlAy7 xlDKzmphpcy7+hUDskr52u5cxo1OEnNQy5CBewJTAEE4bCrNTeZPKyzL/KI506DAtPyF Do0cTmbSS1f8GprQ2izwelIAocDsZ3JzKUkVvHu2zpq9Ezwh945c+A6ScuUsWVhLcrH+ sT5CUOtF28S8vHLdjivhkjr8gv6hys/uPCH7tW5AakZEb5c0RGQl2o0FL1Hq+5Nj1loB OOhIvoPqE1MDAeCFwXeOHmpS5kWzbisSX3iyI/yw4n8W60YdjHKhhj9aVbSKxwZ7Uu/8 z1oA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=PMoZX3ls; spf=pass (google.com: domain of sanz...@gmail.com designates 2a00:1450:400c:c0c::22b as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr0-x22b.google.com (mail-wr0-x22b.google.com. [2a00:1450:400c:c0c::22b]) by gmr-mx.google.com with ESMTPS id z137si718161wmc.2.2017.08.02.02.40.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 02 Aug 2017 02:40:18 -0700 (PDT) Received-SPF: pass (google.com: domain of sanz...@gmail.com designates 2a00:1450:400c:c0c::22b as permitted sender) client-ip=2a00:1450:400c:c0c::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=PMoZX3ls; spf=pass (google.com: domain of sanz...@gmail.com designates 2a00:1450:400c:c0c::22b as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x22b.google.com with SMTP id k71so16467182wrc.2 for ; Wed, 02 Aug 2017 02:40:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=FrdwwPzas7zeFcUiHay9mFBT+gXEFy8NJKgdebodWlU=; b=PMoZX3lshAOIHhcc9GW3ROD6IFmoGaD9KAcUouvJHHiJPjEhjXaRkB0eE4aOzo8kv8 8x0iaMC7waN6buekld5KcsT6+SI63d3iyL1uZo+rXoGeZJbeIl6ZDAQMhlIfrydxKhfR TxkK+qCDjhtw5vvVWoq6cd/3JpJeQJl4qsAh54FQNw/4833rKOMPJY2wnCRuzojfiuhp dxTc+/7UqwXyodjvtuwaxQQ0b1ChNl1ceA/w1S9GwwNuLwW4QenAh99xkh7Le5ERn8sY 77Omg3MIVKR5IZvzmCdze12hUzBAI36RZQluKvsCxmu6jur9cNd2BghRU6rwKazBrcjD 1bDA== X-Gm-Message-State: AIVw110wy5C1mfTL7LN+bcKOnG+UDv+375jbAdSte6KWEkJ8D6ViQzYg ZyZbiKgb2yWg9hvj9TKjwtcObKsiA5ok X-Received: by 10.223.177.202 with SMTP id r10mr16368295wra.36.1501666817813; Wed, 02 Aug 2017 02:40:17 -0700 (PDT) MIME-Version: 1.0 Received: by 10.223.166.230 with HTTP; Wed, 2 Aug 2017 02:40:17 -0700 (PDT) In-Reply-To: References: From: Andrea Vezzosi Date: Wed, 2 Aug 2017 11:40:17 +0200 Message-ID: Subject: Re: [HoTT] cubical type theory with UIP To: Michael Shulman Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Not really an answer, but one observation about point 2: > 2. Can it be enhanced to make UIP provable, such as by adding a > computing K eliminator? I think we would rather derive K from a computing UIP, because even the J eliminator is derived by proving that any element of (Sigma (y : A), x = y) is equal to (x , refl) by using connections (and then using comp on the obtained path). I think something along these lines should work: suppose we add a primitive UIP0 for every type A (restricting to some universe if needed) UIP0 A : (x y : A) (p : x = y) -> p = refl then "UIP0 A a b (\ i. t)" could compute by scrutinizing A: in case A is a "positive" type it would commute with introductions when a, b and t are all built with the same one; in case A is a "negative" type it would commute with the eliminations. It's quite probable that UIP0 will have to be generalized a bit to make sense for path types, just like composition generalizes transport by also having a system. This might make connections in the interval type redundant, because they wouldn't be needed for J. Best, Andrea On Mon, Jul 24, 2017 at 12:54 AM, 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.