From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.40.145 with SMTP id o139mr11081866ywo.218.1501472974959; Sun, 30 Jul 2017 20:49:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.146.87 with SMTP id u84ls7956940iod.11.gmail; Sun, 30 Jul 2017 20:49:34 -0700 (PDT) X-Received: by 10.31.159.11 with SMTP id i11mr9275522vke.55.1501472974123; Sun, 30 Jul 2017 20:49:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501472974; cv=none; d=google.com; s=arc-20160816; b=umzJ9ztsYWDzDfHXJzSH3NIhXK3COnIl5fFkP4Ab4Iz5K0x9tLkUTd3MdHwDvj7m+3 Ek3z8eoRz2Xm4SJfzHsM1r7Shg7uPNkMrT15oHjkoPTlNbox2kLjcctR5iPC/q91Sn6i Vv+Ama+4EppoZq5pchpVIP/PMi3hBSiXp7EoQ8DX3s3PUhgLFAv91lVxZ3W+V7Y1Qpgu 44KEtqnIZ1ERQN13eU2ijDeVS85ijm2LJvVne5kS6rXaALPmP9kxnHdDTwE+JupruUPo HsYHz2HQb553KfMJhU99ay4RtGasP7AG15Pxl8GLcGbcqOCPZBrGuMcomtb0hQSfESL3 fb5w== 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=2MiCA4Oy22tdNOIxkAWoP0KUzd5S1A0ljbxJcdDtShE=; b=bTrvgkbNZgWGwtK4AmUxcnap5/aBEW+qmMKaUC66qN5epaRlx9S5JHAfM6i0B8vPAG heXCIRxeZlzo4DBo1FzjOVUEHOp03TR6Col9BBg0ZYMlHi0PLhmxqUXKRn2kxl9B73yb +hg67wW/jEH+wXLlqa1p3eDhO9ZH35e0vhRwr+4KFNOcvfkehv0fT0qn3vdAVvKYUJsw LriKnAWpU1OtTvRUnIG3pH5swQZ4dJ3uDglzZPBbAVrjjkw7+cUa2mzKUZ28FJBFxIXt gy1bK23DT8W11vC4vZ0WfpM7FTzLILj5RxcZuT+XiStc92eN5XYJjcY1JnvDNDZE5/eX 9PSA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=rkj+pFdK; spf=pass (google.com: domain of atm...@gmail.com designates 2607:f8b0:400e:c00::233 as permitted sender) smtp.mailfrom=atm...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-pf0-x233.google.com (mail-pf0-x233.google.com. [2607:f8b0:400e:c00::233]) by gmr-mx.google.com with ESMTPS id f66si739389pfh.10.2017.07.30.20.49.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 30 Jul 2017 20:49:34 -0700 (PDT) Received-SPF: pass (google.com: domain of atm...@gmail.com designates 2607:f8b0:400e:c00::233 as permitted sender) client-ip=2607:f8b0:400e:c00::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=rkj+pFdK; spf=pass (google.com: domain of atm...@gmail.com designates 2607:f8b0:400e:c00::233 as permitted sender) smtp.mailfrom=atm...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-pf0-x233.google.com with SMTP id t86so5951539pfe.2 for ; Sun, 30 Jul 2017 20:49:34 -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=2MiCA4Oy22tdNOIxkAWoP0KUzd5S1A0ljbxJcdDtShE=; b=rkj+pFdKrMX7c+uYbY1I/VbsswwziVUQkW0yi/GR0Gm7NPeN7e5QN5QoMceeNun2Vv IJA2MDeKTnqe6eMmPZ8WvzgWs7OO6XoQ0sGmE2DQwHnULA4UCgBk1988vu4cxU1YU00L oEje9Zlc1DYFMoeYZDBhpEt6POoah6LoX6Zuhy7ck6m6A6Mb6k+qe6q0+fuMuf3weh7N 6zR9mJcfaVQxjSJNrwstrA9MAO+9VB7r874ZxfGZe95PTWopKENG22t/en3ZLaJKvpii fPR/hXydxTIO/Yi2FC/AAw1A9DA2KewxQmu0zhGswcz8zIjyB6QKLKjCjr2MAJz4gw7W W7+A== X-Gm-Message-State: AIVw111HHv4RQGgfLA3vJIZyIld0pMgmRyImymUD8DKLjZAByrfKzL/o eSvvDmwnMfOObfwZh0q4OAKieZ51cA== X-Received: by 10.99.98.68 with SMTP id w65mr6098943pgb.268.1501472973697; Sun, 30 Jul 2017 20:49:33 -0700 (PDT) MIME-Version: 1.0 Received: by 10.100.165.226 with HTTP; Sun, 30 Jul 2017 20:49:33 -0700 (PDT) In-Reply-To: <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> From: Matt Oliveri Date: Sun, 30 Jul 2017 23:49:33 -0400 Message-ID: Subject: Re: [HoTT] Re: cubical type theory with UIP To: Homotopy Type Theory Cc: Martin Escardo , Michael Shulman Content-Type: text/plain; charset="UTF-8" On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo wrote: > I am interested in this question. > > Univalent type theory gives something we don't have in e.g. the calculus > of constructions, such as unique choice, or function extensionality or > propositional extensionality. > > A very attractive type theory, before we start to consider higher > dimensional types that are not sets, is an intensional Martin-Loef type > theory in with universes of propositions and of sets, with propositional > truncation, function extensionality, propositional extensionality, > quotients, Sigma and Exists. > > (1) What is this type theory? (Whatever it is, it is a common extension > of some spartan intensional Martin-Loef type theory and the internal > language of the free elementary topos.) > > (2) What are its models? In particular (as Mike asks), which fragment of > the cubical model does it correspond to? > > Martin I'm curious what you guys are thinking of doing with this kind of system, and why extensional equality of strict propositions is not enough. Is it just that using strict propositions is bad style for structuralists? Or maybe I just mistakenly assumed strict propositional extensionality is not enough. (Any computational content of proofs of strict propositions is not internalized. So with constructive functions, strict propositions do not provide unique choice.) > On 29/07/17 22:19, Michael Shulman wrote: >> 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