From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.44.145 with SMTP id s139mr10736987pfs.38.1501516278490; Mon, 31 Jul 2017 08:51:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.127.88 with SMTP id r85ls8673367itc.22.gmail; Mon, 31 Jul 2017 08:51:17 -0700 (PDT) X-Received: by 10.101.75.138 with SMTP id t10mr11479991pgq.155.1501516277661; Mon, 31 Jul 2017 08:51:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501516277; cv=none; d=google.com; s=arc-20160816; b=Wv1J3GgUE5N8cyyFNOqQH5dIoAm9w12+wmuyPyVj8cYaH8isSOaFLGAT+GisuJ3pVm Az5CjaAxEaTbmEem2B1g9YVaT3UoYKQcq8i5e8luKWpB7Ha9QRo43S6lJqfMVAEVV12x 6HtpEtvTDwyHCT+q5fORL2NoP6/FgXCDHxm0Ty6oi1qO2xD2avsUpk4QP0ty8TtPPX4O qX0jpnA9IO0JTiT7YFi3r2dnyfKksVURq60m3VxtUfGOIMfUTVZa4qeIoOqPPv9c2I3k qcok3VuJ+fnlE0Q1wptlgCyLgSNiLKIk4aqCbv6n/Xf7+Xo4EY33kVy5RPEB1QGDBkw1 81nQ== 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=518UfaUvVHdEYmU3/KWitRDtEnvwOSQRiG+Awqa3geY=; b=fiLKWLtvRbSWr8tMl4UcBfFmtOxHJltVmGYYc0RT1cm7hqgPQvdHe8WltI9EpFyZlg 89hYkJqW8ScdcXVRsa317jFnfOGzufr8AgobFmhN2McnVzlJg0V3x9ljzYifiQGNE1JS 3Lm3d9VGQdAZBnHvP1povIGgZz5kj7sD5XsUB05LyhjirutlNt2/JxUyZAfPDGAsb+9y 6uAejzQ1cbvvGOmleKUhBdxmKF0nx1bETgRKHUzzcnpsgMkGYtUR+E2xOPWPiyG+jdHS bXXk23w6srfMbdnpEjbk32oghloP2xi7FMV3JR4DxikI0gwXUakOsIJjvTJa7nbeFPtY YrEw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=uunQet87; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x230.google.com (mail-yw0-x230.google.com. [2607:f8b0:4002:c05::230]) by gmr-mx.google.com with ESMTPS id h5si1720662ywd.12.2017.07.31.08.51.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 31 Jul 2017 08:51:17 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=uunQet87; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x230.google.com with SMTP id l82so101038302ywc.2 for ; Mon, 31 Jul 2017 08:51:17 -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=518UfaUvVHdEYmU3/KWitRDtEnvwOSQRiG+Awqa3geY=; b=uunQet87g348ZnRM5E5ikokIUACybEW5LbvuaXV6kEZHXQHNfH3xDjBSA0AWT65nni ZVSEKNqdyGFxqVZbtZ/jxLzMAwvJcwvX7GAsychBk/GoVW4CFOYXGha4H6hzkXJgHHwt 4n+FhlKbSffiN0+YlptgHWda/rQWMsApLKtmndF6c2BVa7YS6FltboB+A0hXk6WmXE0v n0sKqbcuE7GJyCu4CZehK9KPB2Og4ViAaCsE+q7GXvyOxzp4sIaS4LjRaXPB1OGVLT6r dIq8HR0/e0c1MejnuodCScHDkToWMjBGv776saEe4Cf95+YS3Z2/sbkS7/yCGa8YCOAb Gjww== X-Gm-Message-State: AIVw112hKz0Gs6j758dWvN6ACTQsar6Hztamw5fZjLZDblHG5tzmspPS M45U9rFX8RUpG0rwLkM= X-Received: by 10.13.219.79 with SMTP id d76mr15276385ywe.79.1501516276876; Mon, 31 Jul 2017 08:51:16 -0700 (PDT) Return-Path: Received: from mail-yw0-f177.google.com (mail-yw0-f177.google.com. [209.85.161.177]) by smtp.gmail.com with ESMTPSA id f127sm1690112ywc.0.2017.07.31.08.51.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 31 Jul 2017 08:51:16 -0700 (PDT) Received: by mail-yw0-f177.google.com with SMTP id s143so26863001ywg.1 for ; Mon, 31 Jul 2017 08:51:16 -0700 (PDT) X-Received: by 10.129.41.16 with SMTP id p16mr13912011ywp.398.1501516275711; Mon, 31 Jul 2017 08:51:15 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Mon, 31 Jul 2017 08:50:55 -0700 (PDT) In-Reply-To: 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: Michael Shulman Date: Mon, 31 Jul 2017 08:50:55 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: cubical type theory with UIP To: Matt Oliveri Cc: Homotopy Type Theory , Martin Escardo Content-Type: text/plain; charset="UTF-8" As I've said twice already, what I want to do with this system is use it as an internal language for 1-toposes. So to me, that is the answer to Martin's question (2). I'm not quite sure what Martin means by his question (1), since he's just described a type theory, but the original question I asked was whether cubical methods can be used to describe a version of such a type theory with canonicity. Another motivation is that as far as I know, there is not a really satisfactory version of sequent calculus for first-order logic with equality (e.g. not having a fully satisfactory cut-elimination theorem). If cubical methods are a good way to treat equality "computationally", I wonder whether a "cubical sequent calculus" would be able to deal with equality better. I'm not quite sure what a "strict proposition" is, but if you mean having a type of propositions that doesn't include all of them, then the reason that's not enough for me is that frequently in univalent type theory we encounter types that we *prove* to be propositions even though they are not "given as such", such as "being contractible" and "being a proposition", and this is responsible for a significant amount of the unique flavor and usefulness of univalent type theory. For semantic reasons I wouldn't want to use intuitionistic set theory, because it doesn't naturally occur as the internal language of categories. You can perform contortions to model it therein, but that involves interpreting it into type theory rather than the other way around. I don't know what you mean by "somehow clean it up into a type system", but if you can do that cleaning up and obtain a type theory (a "formal type theory" in Bob Harper's sense, not a "computational type theory", i.e. one that is inductively generated by rules rather than assigning types to untyped terms in an "intended semantics"), then I'd like to see it. Mike On Sun, Jul 30, 2017 at 8:49 PM, Matt Oliveri wrote: > 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 > > -- > 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.