From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.146.73 with SMTP id s9mr10571231pgn.31.1500850479185; Sun, 23 Jul 2017 15:54:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.50.208 with SMTP id j199ls765783ita.11.gmail; Sun, 23 Jul 2017 15:54:38 -0700 (PDT) X-Received: by 10.13.215.77 with SMTP id z74mr6931592ywd.47.1500850478400; Sun, 23 Jul 2017 15:54:38 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500850478; cv=none; d=google.com; s=arc-20160816; b=pibbtfbiAw1mmc3h/kCDXSxupl8sksfi5BHCuyhc6/om/gxotVHNhMNDDMt5/EZkGR Ft/GJcbNtmDE66aw+twTox6W1kSzhEukRk1guL0sCghUj0CKtPEGJU4Sl1x+iVLQDReZ 0f4aPr+rGHjVhGvZv51nQqIJffOmbKU6eRV4VTjjfhlRJCv+HVNUjwpPOl9ywRvvN9oS yCnTZ7vQM5y0rmMjz6yQO6kNMhtF9xnIBF3tvjglJYA96802QVqqXCMPyEQHhp9CV3Ie 6v09xUQSH8QNCLsMM7p7pEc2Z/b9aBPmjoUl91Mu74Osof6iBnmXLuTmzdjgpQ+tMSTI wxhQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=GTxzkmko0scJJNQnR+VhGwHuFwncLPMDA5TU9NF0beA=; b=WlKBI97BxudWQGiIlJTzTeUDP0aXuLR/IqgihMs0NzmPX156oCW2b9nVT01/zmhF9Z KhLbhuKSML5zU1MawzQlYlDPQuPJ4cMsQvb+RhIfTDuve8oINFfvoclgrB/+NvlTCE3N KYoMBRZDvUqQO9rY+16hQQrMO+2XIo48t+luj2Wki99tMPCEmkbTpk0Y1+ilWnC+9u7s ugmbDR3rCiLIskK5shNOl618Bhba0NoP4dv1trGxcWdhgkGWeJTGrXj3l843VyLgTqeG PlBs+ZqvhhKf4jhkUGCGDcgLPQ9L/iMi6LhRhWj0VOy8NocnWy6Ja2mb0CsnLXQORZ5X LTWA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=OQU3DnDR; spf=neutral (google.com: 2607:f8b0:4002:c09::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22e.google.com (mail-yb0-x22e.google.com. [2607:f8b0:4002:c09::22e]) by gmr-mx.google.com with ESMTPS id n185si496949ywb.11.2017.07.23.15.54.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 23 Jul 2017 15:54:38 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22e is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=OQU3DnDR; spf=neutral (google.com: 2607:f8b0:4002:c09::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22e.google.com with SMTP id w187so19711581ybc.0 for ; Sun, 23 Jul 2017 15:54:38 -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; bh=GTxzkmko0scJJNQnR+VhGwHuFwncLPMDA5TU9NF0beA=; b=OQU3DnDRnEC0QR8uasqm5vlLNaKXCDxxItOmKBA3lMrSlO49KInBecUhmfCpOSiZnk P47sUwb37lGyTPqCb/hN6I2xjWMLZoqnU8/WOyi40RZ7Ih9UD7niaWzC4M4IemEQpkwK ZyT8QX4zVedYtG35N6sIXg7NBxnacOpGIEsHfl4oECKnwc09KXLNAcm4tbmyNpjxzbok psK5jviuZ72uuogEvSNC3LAZSnXmPl2vfQ54QZLO0BBqkrHOQghQsVCMv62olYGcvvD2 z9yGZfbaabtH/8BMFy/JXdoAfhcJvspuNrQumkYuc9UVBdrvqyMM6ZvRTejFFMqUaqhP DCyQ== X-Gm-Message-State: AIVw1114IubidG7Iys9qsm+QFjw9E98h9aJQuGDKle9lXLSB1N9IMPfy 5Kaq3hL4yA24oGo+Fr8= X-Received: by 10.37.190.81 with SMTP id d17mr12229847ybm.1.1500850478005; Sun, 23 Jul 2017 15:54:38 -0700 (PDT) Return-Path: Received: from mail-yb0-f179.google.com (mail-yb0-f179.google.com. [209.85.213.179]) by smtp.gmail.com with ESMTPSA id c15sm1525433ywa.54.2017.07.23.15.54.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 23 Jul 2017 15:54:37 -0700 (PDT) Received: by mail-yb0-f179.google.com with SMTP id w187so19711544ybc.0 for ; Sun, 23 Jul 2017 15:54:37 -0700 (PDT) X-Received: by 10.37.219.148 with SMTP id g142mr1757649ybf.17.1500850476824; Sun, 23 Jul 2017 15:54:36 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Sun, 23 Jul 2017 15:54:16 -0700 (PDT) From: Michael Shulman Date: Sun, 23 Jul 2017 15:54:16 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: cubical type theory with UIP To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" 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