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-pl1-x63a.google.com (mail-pl1-x63a.google.com [IPv6:2607:f8b0:4864:20::63a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4633a017 for ; Thu, 14 Feb 2019 19:05:08 +0000 (UTC) Received: by mail-pl1-x63a.google.com with SMTP id b24sf4955691pls.11 for ; Thu, 14 Feb 2019 11:05:07 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550171106; cv=pass; d=google.com; s=arc-20160816; b=bNdcW22/uDRLzP7M0IoLp/4gkeFRzAAGl0GlK0sFN1MVUxaIB6BTsgeFhI5ToKQ8CU n/+6E2jGqGizH61necZEMxtkWhQAmihSAMYX8fzkVIW2Wn44lkFiUdS7qBppL+40YCWM 6SOyXTgqZRyLnglRAC+5VmWWkknuRX94OpNY4YQw4DrK6FMzNx/Psg4JWg0ZAHeon3Pu hCveQolNyNA19VPiqIUNMUdWin8fw85cdVVB3EonEk+6wBICkknrERrFDcF4yD6vMhT5 mpBWYdGeOvWL6VBTViipsjT2BPO8/rH5UsTcsReJ3/ODATTenTVzMXh4H2gDI4EQ28I9 RNPg== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=a0ucJNDnJZB5Z/F7KiY+rfS2ZRDLb34TGEcncC1yUZ0=; b=mEUvu3/Z3LI/c5dTa10/+/Mwn4wRuVNdHVBVdrcGfKdOCtV+MP2X6hVXYh7SdEpIcR sDOuOFgjMLpzG/+NIdkaoHsQ5EuKGgWQh4ycnjA41Olr39LG0v+AGpKWehV0OBtzMdHO AsMBs7zxjELROE3eyeZRMQGk4vSVFUEffC6YZsJlvjBZVnx9W6KNYdiUO+FZgOktuS47 PxqDmVqNHWaL4UV8K1kWG4hQtPWF2T4vQfo24ugUJw3YStdzyxz+xaKr94eZPZbkUe3S CLaoGSDAro1twAmNqIdHy2IZWTdiCMDeHNhW6GiWu9AeTzbSwiZU2+OIQXBFeJqLXswd QnUQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LNanZkD8; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::342 as permitted sender) smtp.mailfrom=andersmortberg@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:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=a0ucJNDnJZB5Z/F7KiY+rfS2ZRDLb34TGEcncC1yUZ0=; b=eJEkVQbeXZ8DsEN/6dVSNuflYrqgq0DUXPbI0MSZcvMPM74/YOS6fb2SGJrKxha27J Vb8HgkLL6oYipcJNNyr9gG28G1vAMd3pfyNdo72kUbTKv8rNaPUsXq+IhxUwBNu16qIn HMNaEnmADt0TZ7fynPNbIGpQYBvjyGtE4XZZThZTGYaEcf6O7TbRWUdLT+XOfau7LmKi YUCtrXdMcCnrcLIAUSRuWuMfL1aWeiRlvfkl25iiZ6/UrwJPgkjuFewHQMNfhCqGxx/m 5WGP5jsQtROthqnFYoRSZYpg13ntV80TfHa2WTw02A5SfdO97Tqiaa2A0eluyRciTBuf 3FCw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=a0ucJNDnJZB5Z/F7KiY+rfS2ZRDLb34TGEcncC1yUZ0=; b=WskZpBYwdYrgCL5OGsFBx02QcylxszModv97B/0izWuIDULBrlV9N8Kunhr2mkZ3x7 QsrRNgk57v/EXw72MHJXOBY7IG/csSdXANoAzDTRNSyyBWVp0wsMTh23pjJex93IcEOq NADToSv/WTPE9/8hlkhNO+DslVOkvbLxLN0Tq3cASYY5OCW151DUJcHxhg59YRxqHx1L XSWXd0xMzzfYBHugUDvCXk0aMzowMT1qM86n7vor/EWLmhrPBdevEgu/SBIbxpMQDX5y k5ePjqD0xXhKs+zthMNtMBqAr5nvYwcqdjHEMgCXR9Hec+UUADhsQ89rJbf39tZoYUPU S86w== 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:from:date:message-id:subject :to: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=a0ucJNDnJZB5Z/F7KiY+rfS2ZRDLb34TGEcncC1yUZ0=; b=PfzwpVW6Cg+8S16UiN6t1/nGzHIU+y8KEolDmNhGmyFYy3GRe7zGzecog/ksryjF2P rXOXCdLPNZznAEMiJeXrbTcZBlmeELBeATzf6gLBmIZ9suYCwY6ijKCJ+PBm7l4VrsYs ODvm/GF/PlInF9h/rRYt/47s4pzOLZgcr6byQrvFYFKHEgBxlQ5RFjxs9E73+pY0Oi1K cVXJqYIq24e9lKixWJBuKcubILvqoawIcT/DXTm+C4yMshMhofrvwxpBMqpARBIY5gcu W5ptmXzclMK6gVZTp3CuiftnIzsIxP+1x50xlhbRpp8uPwoJcG3P2O/BGW03VScGeYeh 6CZA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYswhnnFQt0NFzcclw+F4GqL43EyarWOfrsanl8Wo0VUEsWt6kn N4j3Vo9EV8h+cfqUqe+C9b4= X-Google-Smtp-Source: AHgI3IZrgBTA7t8uL3PLubFL+nX2huT29wX5BD99KZDlZ+apwvQiO+JJmQh21x3wAGb3T+zIMC0rEg== X-Received: by 2002:a17:902:7089:: with SMTP id z9mr20295plk.6.1550171106594; Thu, 14 Feb 2019 11:05:06 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:26:: with SMTP id 35ls1897313pla.1.gmail; Thu, 14 Feb 2019 11:05:06 -0800 (PST) X-Received: by 2002:a17:902:1aa:: with SMTP id b39mr1697539plb.139.1550171106289; Thu, 14 Feb 2019 11:05:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550171106; cv=none; d=google.com; s=arc-20160816; b=mOHtwVAGhOEBG/brvThUmo95Rlq6OQdOAAD/XqNF9SBXuYE2NHJFszepUD145pHnf0 I/pgnZW7+xIn33ealOFalBRHw106XRXkmNHwaPZz2PV4K056lDBVk5eHW1W9R2/oxokF miKskvXXpa9nA6yKcpM27IoJxk9qgqhBMqehc2LM+UhTaTtvFKshULoIjUqeK11WJLjg slV+iFFWCOchKw2ValKLPeF9TWrHtc286Md0NdWsxKGDE/cECIqMBQVUbMT1l4K70Tfn nHrIzCqpJJfyf0IvRQQlPsKpamei+4JGZiyt9Leb43RmlBcIWkbNDtXtQthWd+Hd9zol V9zg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=fYmn4hVOYIVr6+GbW/jxhnqjEwXHj9jgV/Me2+4wFXE=; b=rEjSDDDXpIdqUnRenTIZM13Jc+sGjkUY1ED3Kjyu7Tqddjc/dLxBVnS/sdqUz/NA8Z 4gbT5ZfvqMUr7X1XFRBQ6xSzXj9CVM6yz5USpEYXyy3Koh7esS2VPkeuJOkZEh3iREKc odIo7x1L4k6BtPVLmXDlg7DvyPjOBmyw+D9MbkgD4Wut4FztqyrNisUDr6U+zOl46Ys0 cadBlERCsPKLc+RUFhITbPxh+OJ+orVI+r1rdlgP4z+4+YEvcJAuI2yeGDVQZa8P/0rY 6r956FdEd9Ejc6j0yoQYQUmRRsIjMoinl6Kx2HEBLJUaf6ktaUD61h5KjnxTYTvpyhdv 08EQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LNanZkD8; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::342 as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x342.google.com (mail-ot1-x342.google.com. [2607:f8b0:4864:20::342]) by gmr-mx.google.com with ESMTPS id t14si189458pgv.3.2019.02.14.11.05.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Feb 2019 11:05:06 -0800 (PST) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::342 as permitted sender) client-ip=2607:f8b0:4864:20::342; Received: by mail-ot1-x342.google.com with SMTP id z19so12414776otm.2 for ; Thu, 14 Feb 2019 11:05:06 -0800 (PST) X-Received: by 2002:a05:6830:15ce:: with SMTP id j14mr3425347otr.82.1550171105612; Thu, 14 Feb 2019 11:05:05 -0800 (PST) MIME-Version: 1.0 From: Anders Mortberg Date: Thu, 14 Feb 2019 14:04:54 -0500 Message-ID: Subject: [HoTT] A unifying cartesian cubical type theory To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LNanZkD8; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::342 as permitted sender) smtp.mailfrom=andersmortberg@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: , 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.