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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-it1-x13c.google.com (mail-it1-x13c.google.com [IPv6:2607:f8b0:4864:20::13c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4f412fe2 for ; Fri, 15 Feb 2019 08:16:57 +0000 (UTC) Received: by mail-it1-x13c.google.com with SMTP id 135sf14499041itb.6 for ; Fri, 15 Feb 2019 00:16:56 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550218616; cv=pass; d=google.com; s=arc-20160816; b=yaXUjQzwLxaMIPT3lMYJly6CszhC1XP2vOeACGxaLb4VWbNl1ODcmxplKhXLvhFp0K eGW9RoVEwleGdqHCiqNa1FYTB54o9pCrVSMa9mfzS2LDz/kMcrEhwloKj5gN7wrPpRF3 YfhDKzWY/8sfL/jqQ9GrR48NIXUnA1/DtkbiDQtJQaonbcqlE/9vgUpK4QaVFYlfvASZ QOuuzhZYidEwxQElph7h6IvhQ/YHTSVXJh4tSLXc6wRTwhdIKcD7SpwjIkKc8w1kvUNr RKp57jBfpPHv6Z4VkaCdWFrBLsClqiu69HHOCUkUf/LAU+6zJmj6EqOl/a1KJhGkKyXj UTgg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=Vup7fH0n/e0AYI6OB8M7b/fjq+YBzuJCZBSdQYJGIP0=; b=JtoKJDq9erfiGs+us4HCE7QNHPsbruGqG9lPPwrCiuUIHOoz5Jcs42zXEzbX5kZXGM OwowJ50szgUVDqQjeBe/L5DyArED9KMmtD5WWDdjWy3CGjB3124d4fjCIMdeIdB2+ceo 9NOdYq6znt4N9PW1g8Spv7rAhNaVPRfqxuuEoCFdNhkCKAuusj0G2esK2ULpCXsc8p9U f4RY1RpMxJx+ORWgBIUMqkisBUbLELHvtg7RkTG6WVHrsQSHX0RDenmuCilPIRofG8QL CyfBaddfldzPgTw+NG5Xjs3/Etn6AfhuMy73Y/EXv+aYvzEBONv73fha1vgop+E9XFcY z3YQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XXCSKJ26; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Vup7fH0n/e0AYI6OB8M7b/fjq+YBzuJCZBSdQYJGIP0=; b=TnFUz2QN0kfBBeREyegHsFa7lUUKqT0nPudU+lD4tU35ysrHdMikKuLPPy25Jb76Zs F8bpQZtqndLei9FWxeLSSVAXVBC17mx8mfP3lzuENiN7NIkiyUPRk+r7s1E57MJTsyLZ rnodJMytz1xuWzBNWwkbnifX4yxkEXQwtc4bH6CHAOOTYzeaUiubqDv9SdwTrddEZJw7 zGBgYdEcfIMSBvmuUmHgiIvqH71QHRqXN+GxNjSb6Swob4MAct6gdIdWLiVwclH766rN 21DnL/K/VsZ11/t4QrJRtCyLuoDkUVyqFpYluvVGXJUbjpUqKpYAnBRI6YPwdVHrEAxG CT/w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Vup7fH0n/e0AYI6OB8M7b/fjq+YBzuJCZBSdQYJGIP0=; b=fx4DFBZ4TxXGMufOUlZDodnAM6vQnZmOmysLqw1G6vEnRXPE0dpaGTa4d/xxfhEIWr r+zPgV8H3FZLZzUY+a9rHuDWQOmqlRPVBjXjtL0/OYB80X9SYYVbrZWi1hpyjPgkYIxt 1XW756gmgwxacMV4fbxCeMj7KJG+4mNHUIoV9c4sGTV9rwXsI3FwzBz/ax4p//3glHpx 1IrDvtvyWZkusbiMuVGNV4O8pQ5Ep47RbHoQKVW7X36dXGLrLeY2V4B5m89ncqXlGbei h1buJKdsfFZAedgLwxmOsLThQuthF9Wmj/EAqkzxrVnSkTRWrKxz8ZZ8zEl4pdOPqz8P wUOw== 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: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=Vup7fH0n/e0AYI6OB8M7b/fjq+YBzuJCZBSdQYJGIP0=; b=XYURd+MGMPCRP0DcMe2Ns18lywrlkRFjCTNOzeB7RwGef1sumj58kIX0G842iOFGGF pGCqDmx9lU8vlMevZQTi+1X3+2vFEOGuamOuiyKwwuqAAVGxBMuVpNv8K+/Sd6P3n4Db nMONAD5MZr/zf3R2N3DTRB2humCn59NU0vl6kauRXLi4j3tGtDrNoDC+UMFLKmP4XxcN f3oqSqiwLf0jlu1NC73kPXw1i5hrQGSBFB/4O8aSim5M9w3J1kJlH2fWmVNQEvxWeNnz tgKm5GTYNeji75g3Z+PufLwWQPxiS1H+6j35FIOI5lZGQMrzm2aOblJ6WK0TffwGEMo/ OK8w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaFO2gACk+V8a76I8QdMPC3xV4GL7p3gKXqTsYQy9CGVLXktbpu 8cbf3XLxaXDM/MtKVjnZVtY= X-Google-Smtp-Source: AHgI3IYXEFT0Wis9dUt+ZsH/SMMEuHyY18Y7OjhOlGo3OYSxY+jYBbnIiPRWDSqGD6QVZyp6d9uq8Q== X-Received: by 2002:a02:9b36:: with SMTP id o51mr45724jak.3.1550218615874; Fri, 15 Feb 2019 00:16:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5e:8303:: with SMTP id x3ls2061656iom.3.gmail; Fri, 15 Feb 2019 00:16:55 -0800 (PST) X-Received: by 2002:a6b:7d0b:: with SMTP id c11mr6135260ioq.23.1550218615620; Fri, 15 Feb 2019 00:16:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550218615; cv=none; d=google.com; s=arc-20160816; b=FL6fcCJ7UBUicdeRmaI6ezeX6NfbgNiMogVQei7vdox0xz7EDRaT2O/DDWQ9qFCl6i 022mRJy5FlaI3g1AUb/aB+csekNfHYanfqjbcyE5YQgM1khMp7PhI4MKbANd6LIjNHsh muTxEzqu1ZsmrL60jn1EDxjlw1BjGEWk0K4WQHIMeiNrtQsMBprtbCo2TLCyFWGtwEvd TclYrQZU01di20U3pe1awxgKGQ8/4OSHORkelSraQZ6662HmtuKUVLu3Ho55ycXCiTOR Zpt1fOUEpNlKJmoNXOB9re+e3dwMPDa78qGxKmo2Ntonkv+QKvqGWdIb9aSVagIq0MUj OcNQ== 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:in-reply-to:references :mime-version:dkim-signature; bh=yUiry76cxreReQx5JRLcTshxHK1BdWLq8v+/BkdIzYU=; b=iNyNXK77iEG1IJAnhftSm1cuZAvR+5M0aeJXO3aKxD9dqKWNZFyolZ6lIySnoepAkr 4BmedE1QtbnbfMKn9tQAwOCd6eTgUB61TCTczzeFtZ5wG0N35jd98WBf3wii7uBgn+7V jwU/qUcvA1wMAjwWjK9T1QaQrsei9KUnQcIVGCaK7rXUcHlwN6KWSoGGFI35GtA7EnaN zUij8vWUfSgykpZrLPMHocGjiTPj5mttQPlf9mTW1ZlEKHhQm6cyrBlqtyhpO1eVwaaI igXBINphTT0eiFFUZdWUT8AalZESiifu0NkA0LmhEJSiAGZ3wZKeo2v2CAXb/1pUaYKB wxAA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XXCSKJ26; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yw1-xc36.google.com (mail-yw1-xc36.google.com. [2607:f8b0:4864:20::c36]) by gmr-mx.google.com with ESMTPS id 2si242720ita.0.2019.02.15.00.16.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 15 Feb 2019 00:16:55 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c36 as permitted sender) client-ip=2607:f8b0:4864:20::c36; Received: by mail-yw1-xc36.google.com with SMTP id o184so3393718ywo.5 for ; Fri, 15 Feb 2019 00:16:55 -0800 (PST) X-Received: by 2002:a0d:d182:: with SMTP id t124mr6770461ywd.268.1550218615284; Fri, 15 Feb 2019 00:16:55 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Bas Spitters Date: Fri, 15 Feb 2019 09:16:44 +0100 Message-ID: Subject: Re: [HoTT] A unifying cartesian cubical type theory To: Anders Mortberg Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XXCSKJ26; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , 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.