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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 767be1c2 for ; Fri, 15 Feb 2019 16:32:11 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id g24sf6437285otq.22 for ; Fri, 15 Feb 2019 08:32:11 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Y2sayICD0o/HA02bmv37GvaAq+KLLAAnOh/Ytvog6pg=; b=bALrOpT+IjJH8KhLylkjWo86u4x+nZuxgRF+m1E8N0h7U1Ukvw7EqHImOVqUCLg1GH 3Im6pNePbMJ0DcYbI7VNxEliinuUfkgArGPRBmIv1HL4hy3/RbM6kXCt8ZU0M3RtGwmX u20yDnOO2LIU2SDb/atmc7L3MnEVGgLpfP65Z2xy1iPjHE/ZntI6NHboDBFq/yGaWqVS 1GxAGMMIw+dDJNv0oUMFG884M1m8x856ZTLttExBSZojkVW5f+/BFaS/ToMEZa0Kal9x Wcj84PMjAlJ8DVL4nbblY2slD8bODtLu2vDDk8NyUffuHe0iJICOiFqq8GBQyY+uynI0 AiWA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=Y2sayICD0o/HA02bmv37GvaAq+KLLAAnOh/Ytvog6pg=; b=u6nSaeuU0tsqKyCb/ty5DnYclkvLzt43EVpt9+ZYehD2Os99TryZpgTzO+mWtDKRi3 3/4tjCLZxHM4nCZ7fNbOHa9lNfS+qqEpT3LaXtPA0TRo9nTsw1QepribNwVPJ16iPDJP dnn2aiWgfsj0KCMKsDhwIMUp+gLosg5sOn9gPUTMPQIo4E3PI8ZUGW2sCcMzzclFL5H+ vWKk034PhwLo4y77KLt91TGeVF5xgJk44G7vhY4DeUTbEWv4xjbrtE09a1F/N9hGDrT1 JWwgypOX13AAM0UH9IZ+c3BsES6a9DY4EBY5koe/Nr1u/IoCR3YluEjj2xbtm1h1GO57 VqTg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=Y2sayICD0o/HA02bmv37GvaAq+KLLAAnOh/Ytvog6pg=; b=fTkmGLycKhUSigcAVVSE8zsjubPcLTn8tUCFuATYNtzEDN4ioK7w4LKs0p7bpiPXf2 R5eGjlS4u0YC7zTWmKNHJsqe8QJ+1PQImrpoJIPnw4gVsT+C8OKO75Yb+jgRIJvRzRM1 ki0lIJugfAAI/En3VuOTKkCI2Ssq4N1ekxxABhTT5VwMA50nWc/9AoesCTrp/lTrTATD /wcZwWEJW3CjEoe99bI0S7d8scSlvi5JHZdlAGAv2G5gL/b/YgrbZUUAXXejzezLB7Rb ntrCiqSpUy1FEqB/6WoQBBFijd/Ragtncc12bBDq8aeQ9yeb2VpErBjZwY8ct9qDXhT1 s0Pw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubEyXk8Qi+KMMMzcCzFDzDQeI5BGFkE1muiazEFDh9a+k0QFIGT c5rP7ThsjcBzaTQBCyPTHK8= X-Google-Smtp-Source: AHgI3IZG8wcFVD/XBMJlt4QJM58wTZ6NaPy0EEOobNFGsDUiULap8n7Ut2xZy1784iO0uHHrzJrtcA== X-Received: by 2002:aca:afc3:: with SMTP id y186mr102347oie.0.1550248330744; Fri, 15 Feb 2019 08:32:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:f3c5:: with SMTP id r188ls3950117oih.8.gmail; Fri, 15 Feb 2019 08:32:10 -0800 (PST) X-Received: by 2002:aca:5884:: with SMTP id m126mr97518oib.4.1550248330080; Fri, 15 Feb 2019 08:32:10 -0800 (PST) Date: Fri, 15 Feb 2019 08:32:09 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: [HoTT] A unifying cartesian cubical type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_368_1041690672.1550248329434" X-Original-Sender: andersmortberg@gmail.com 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: , ------=_Part_368_1041690672.1550248329434 Content-Type: multipart/alternative; boundary="----=_Part_369_128685505.1550248329434" ------=_Part_369_128685505.1550248329434 Content-Type: text/plain; charset="UTF-8" No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for 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=s. Instead we introduce weak cartesian Kan operations that are > > only the identity function up to a path when r=s. 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 > 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. > -- 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. ------=_Part_369_128685505.1550248329434 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
No, we didn't think about model structures yet. F= irst of all one has to figure out how to write our Kan operations as a lift= ing condition (this is not entirely obvious because of the additional weakn= ess).

The observation that the type theoretic= model structure on De Morgan cubical sets is not equivalent to the one on = spaces is simpler than for Cartesian cubical sets as we have reversals. The= case that is not known AFAIK is for 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 wrot= e:
Thanks. This looks very inte= resting.

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
<andersm...@gmail.com> wrote:
>
> Evan Cavallo and I have worked out a new cartesian cubical type th= eory
> that generalizes the existing work on cubical type theories and mo= dels
> based on a structural interval:
>
> http://www.cs.cmu.edu/~ecavallo/wo= rks/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 not= ion
> 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 whi= ch
> also clarifies the connection between them.
>
> The key idea is to weaken the notion of fibration from the cartesi= an
> Kan operations com^r->s so that they are not strictly the ident= ity
> when r=3Ds. Instead we introduce weak cartesian Kan operations tha= t are
> only the identity function up to a path when r=3Ds. Semantically t= his
> should correspond to a weaker form of a lifting condition where th= e
> lifting only satisfies some of the eqations up to homotopy. We ver= ify
> in the note that this weaker notion of fibration is closed under t= he
> type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glu= e,
> 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 prob= lems
> with extending it to more complicated HITs (like pushouts).
>
> --
> Anders and Evan
>
> --
> 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.go= ogle.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
------=_Part_369_128685505.1550248329434-- ------=_Part_368_1041690672.1550248329434--