From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-it1-x139.google.com (mail-it1-x139.google.com [IPv6:2607:f8b0:4864:20::139]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 966e8592 for ; Sat, 16 Feb 2019 00:01:49 +0000 (UTC) Received: by mail-it1-x139.google.com with SMTP id n124sf18627034itb.7 for ; Fri, 15 Feb 2019 16:01:48 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550275307; cv=pass; d=google.com; s=arc-20160816; b=MDdo5JkYSlRbwZGNr0csOIwFNRTQWGyRpQuFj1IZvREw/DUrT//XJOV+wuE0XiYQ1u dQGFf4uOWNnN8opdP7gxiNxw12KgJ6dvWKlSg/dooB+sJBdPhnO2lo69LV8pRvnb7cJR vZzsjfxWGLrA0NTsA+vBXDLM1vqMxXek3x0wJsck5QBsMkGiml6STgfcTcASSCke5/jQ ZJsvnstvsmo2bitJ3MYWzSGrsow9AXtWNGqt8w2BqwZuj36iWjjI31TSJD/T0DKQdZlx n7rYgm6tBNjig5G25vetSfHc8FLFLctjdDSlchS0vkm9WukZAvxG8jszXEMKOy0Ug/Iz FSuA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=6/jx8nRgXvVsJOuwCDDjsGLI+CUHJ+a+oN4+iZOHUms=; b=dbkAB1q77qBj7xsEIC3i9CTpJqhb4O12HlUzQHdQyaRoIuOLO7MRDg1+t7QFT2pA/u OnF7IzTieAiLg5laIVTDh/s7CUqSL6Cje8I81qWxTH2AQM/2t7cpeAgpBLjsfSdauxwi 7Al2bQPKaNVGVeE0FAgiCxklk9ip63+DKjYOfE0uRQCQRPKd9XPFT1uxI2trFA+fmtKj 0CuR/90SmnmOVjp0QbqI92qlnmMc50An5VxB1FjlZZgHOTX/WhyBAICqqvX4K+qKeBQL pvUbYjUzrEsoIql9UwLbHAe7ttX6tjQ2a1G5xd28PfWbfMEZw2WefFgM+E5jVkvXmBAu BQLQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=waLloJdJ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c43 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=6/jx8nRgXvVsJOuwCDDjsGLI+CUHJ+a+oN4+iZOHUms=; b=lt64tU2GpJLFZvRRLl+g9fRq7XFEbewl+hlPwCYhACuUhwdvOIIsKCzfwUmR0b8T4/ PESnIP+cIk6rg3IF5njimy715QzJ7j+H8qYKtnuju0jJQ9y7b9G8TmXiAuIPMJRtIJzM rB7IjmsxuaSSF2ZeqJZnGKrQd+ypBjlku/6qG/umNcYEwLm3REFkMZkHeWq6+ceyFvc/ hRWsmMeH+uFpIaIKr+6XSGnuLTEgtZsjmeGxaQwjJC2dcRs3zNhT6z6/kePADBEKeFeu XufBL/o9ZTekUr7qUVVMR1C6icvPh36JQrP/4tk9aSPPPDbqNvhrHG+ElMC/T3POX6kz 6MpQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=6/jx8nRgXvVsJOuwCDDjsGLI+CUHJ+a+oN4+iZOHUms=; b=ot6Pz/YeP8gWMVWwYxqowK1KR7ZWFg1+BV9WscjjRIGWRFY0sEyleyrS+wfYd0qGl+ jnq7I6kKPvObDwOZZEjpGHUXSMZ1XLfnt3GSONhnh6O4Rfe0zZMZWTZfJ/XMed5IZmXS LNk10DyxpStuDYiIev7ag3LmQh3iT88QAt4/NivNMsrMr9n56fz3t+UC8zEAQGR4+eCd mWwALKuHAIXtYtIP88g44QRb9Cadf2/r1kkeL85CZt8qhZNz4KXgEmchoa9Pbqpq2OSz ZDfqcRWcQ+mdaqcOKp5W0/C6EXy0/uUQ17bXYz+h7GUANekOh1ceYYCgRQm4OHGxkAN9 EWyw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAua0p0RZVaPhIdnXS9FGquXIjIdJTOrU3LhFyMiA59BRYJkhc4YB amiwNN687lAEWAGCSjsGIxo= X-Google-Smtp-Source: AHgI3IZc/xTXC2SP7So+iPTajtR6936gFQbGeRzOG5vmI+djvU1MiFvYgwVdhY2S4R+EoOYS+MXR9w== X-Received: by 2002:a6b:7513:: with SMTP id l19mr47186ioh.0.1550275307335; Fri, 15 Feb 2019 16:01:47 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:688c:: with SMTP id v134ls2127875itb.1.gmail; Fri, 15 Feb 2019 16:01:46 -0800 (PST) X-Received: by 2002:a24:4a0d:: with SMTP id k13mr6847544itb.29.1550275306771; Fri, 15 Feb 2019 16:01:46 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550275306; cv=none; d=google.com; s=arc-20160816; b=f3IFzA/b78zrgYaT7PwlKi7wObczbN9CumljDf7BpsFPUOccMNTkP6RHbCj98EcRGc q/6XwZQJteG2y2FyOmzGjg52Bi8mnGkNvGlq5DfqcpOaTAZePE0up4KuatX3RbrhMUQX HmP/Ny6pTfru5NuPyUVLGMeK3zWn0Db5sIghIjp86DP19iF9gYlZ8lr4w1pY9Y/y5Bev 5iRsDM24FBnvyUeWY9GxtcNk3Gu9HB89exbNQ7Porr5029G8hbl6lqSSM2kg4U6hJmDc cj3K1idyrCQCSpEQnpBncxqxm8KcSwxeyR5b7Qv93cndgmqOhU8hmO5V6zZmoXnywa+X IXdQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=N5jY6RrDSxNQ2O6BHOEBpfQFW84tACKFgGP7CPh+xTU=; b=YIf1J1BJERgdYzqITkxtQpocmNiRPurIj4tja+IdSLl7dVDug+t+ucvezUTc2a3uTS PIfl1FpexcNbyAkz6W07v9qQTeDPm8p9ODYyxZH7Uju5/5/jOJeM6P34ZslsiooeTW0k q/tPMLCxqdy8QRiH/+3vkXCbP3P5hi5HEY2Cd6rkvEVRZnKHA2ld8muIYF80c6CpZ3ID iXvyZI2srMHqTHMjl3ZYKycAX2QTmihgxqsCuK4Mnf3AW2k3FM7phFXHkNArYh0wov1h DCd69wRfqFpc4Nwi8sZa2EnzfewoJcop9AXz0Hj4tzK7QtMg8gvOc+W01Vchi03UWm17 UhzQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=waLloJdJ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c43 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc43.google.com (mail-yw1-xc43.google.com. [2607:f8b0:4864:20::c43]) by gmr-mx.google.com with ESMTPS id l193si452177itl.3.2019.02.15.16.01.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 15 Feb 2019 16:01:46 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c43 as permitted sender) client-ip=2607:f8b0:4864:20::c43; Received: by mail-yw1-xc43.google.com with SMTP id k188so4381093ywa.6 for ; Fri, 15 Feb 2019 16:01:46 -0800 (PST) X-Received: by 2002:a81:27d5:: with SMTP id n204mr10013216ywn.495.1550275306368; Fri, 15 Feb 2019 16:01:46 -0800 (PST) Received: from mail-yb1-f173.google.com (mail-yb1-f173.google.com. [209.85.219.173]) by smtp.gmail.com with ESMTPSA id k64sm2366396ywc.56.2019.02.15.16.01.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 15 Feb 2019 16:01:45 -0800 (PST) Received: by mail-yb1-f173.google.com with SMTP id x13so4479169ybm.7 for ; Fri, 15 Feb 2019 16:01:44 -0800 (PST) X-Received: by 2002:a5b:407:: with SMTP id m7mr10068110ybp.202.1550275304442; Fri, 15 Feb 2019 16:01:44 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Fri, 15 Feb 2019 16:01:33 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A unifying cartesian cubical type theory To: =?UTF-8?Q?Anders_M=C3=B6rtberg?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=waLloJdJ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c43 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , Please don't call these "type-theoretic model structures". There are many other model categories that model type theories in ways unrelated to cubes, notably the classical simplicial model categories that model Book HoTT. Maybe something like "cubical-type model structures"? On Fri, Feb 15, 2019 at 8:32 AM Anders M=C3=B6rtberg wrote: > > No, we didn't think about model structures yet. First of all one has to f= igure out how to write our Kan operations as a lifting condition (this is n= ot entirely obvious because of the additional weakness). > > The observation that the type theoretic model structure on De Morgan cubi= cal sets is not equivalent to the one on spaces is simpler than for Cartesi= an cubical sets as we have reversals. The case that is not known AFAIK is f= or the one based on distributive lattices (so only with connections, but no= reversals), i.e. the "Dedekind" cubes. > > -- > Anders > > On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: >> >> Thanks. This looks very interesting. >> >> Did you think about the corresponding model structure? >> https://ncatlab.org/nlab/show/type-theoretic+model+structure >> >> Because, we know that Cartesian cubical sets are not equivalent to >> simplicial sets, but as far as I know, this is still unclear for the >> DeMorgan cubical sets. >> https://ncatlab.org/nlab/show/cubical+type+theory#models >> >> On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg >> wrote: >> > >> > Evan Cavallo and I have worked out a new cartesian cubical type theory >> > that generalizes the existing work on cubical type theories and models >> > based on a structural interval: >> > >> > http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf >> > >> > The main difference from earlier work on similar models is that it >> > depends neither on diagonal cofibrations nor on connections or >> > reversals. In the presence of these additional structures, our notion >> > of fibration coincides with that of the existing cartesian and De >> > Morgan cubical set models. This work can therefore be seen as a >> > generalization of the existing models of univalent type theory which >> > also clarifies the connection between them. >> > >> > The key idea is to weaken the notion of fibration from the cartesian >> > Kan operations com^r->s so that they are not strictly the identity >> > when r=3Ds. Instead we introduce weak cartesian Kan operations that ar= e >> > only the identity function up to a path when r=3Ds. Semantically this >> > should correspond to a weaker form of a lifting condition where the >> > lifting only satisfies some of the eqations up to homotopy. We verify >> > in the note that this weaker notion of fibration is closed under the >> > type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, >> > U) so that we get a model of univalent type theory. We also verify >> > that the circle works and we don't expect any substantial problems >> > with extending it to more complicated HITs (like pushouts). >> > >> > -- >> > Anders and Evan >> > >> > -- >> > You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send= an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> > For more options, visit https://groups.google.com/d/optout. > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.