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=-0.7 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-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 518080fb for ; Sun, 16 Jun 2019 16:04:42 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id l7sf3712430otj.16 for ; Sun, 16 Jun 2019 09:04:42 -0700 (PDT) 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=6TgwVV049I05Dg6p9kbQFicWHyU13pqZlXjb94I89lE=; b=iMHUg34qVOZGy3ndxcHZtb4TeT+rfsXiG4OfZ3D7vIPWP1s4JtpuZR25xQmTi4+0Nm HHxnZOfBguecGsT3GRg1S8vAsAhGOC5YepYDYuz5OHfaiJolGuGDFBaFo5qmCNxB7INg EJddGyYFRloCLaiL2P9ntdZ1Y6EPch0qLPO/DFoYUfaKuLgNCsThIHiHL9Ft2c/u+MOG NnL7MIK6jeLlIg4qBCLOcaW0++2ifO5T/vP0QjRJjtFILLMNwF0uZHBZBcfjV0EKmY8U GHp450Pm/0rR/OAaJ+Ztd6z5NokWsDCCfSafMTDpMzvZ5S5nLQjmj6+4XU5zDoMXJ8sH 4cYA== 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=6TgwVV049I05Dg6p9kbQFicWHyU13pqZlXjb94I89lE=; b=uep2r/MuJ+FZ4meaMHxLTRm3hKfpSK8mHA7I3oRHta5BZOpPdlzWIFWVCdSzgkR6t6 yyJZIzyD1WDLQCAiXC/qO93McBtxBIO8x0KE2fgjpcs8zUzq7APq+AF+AUIV+KX3ayad sHr9B6RSvoHAGOM0HpOQ71hC8NNX5gRHZkuM/2p0vNreCcYm9+LeyGi/FBArZCTIs6YT C7a2d+DSPT+XEPAp/I2H2D6CkxHM4E4+Y+qEAd+5HzHHHD45vOx4yXqkdpAXXIlpqDA1 OBA7DiAzfEtVZ6tGh5Qn48XO7wwTF1UB6ymsSgGCKIhccdpJB1EAk0bE4WOJM5MDX0mJ pfSg== 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=6TgwVV049I05Dg6p9kbQFicWHyU13pqZlXjb94I89lE=; b=rMlQ8i+WQdlpqx4PpQ4Qnpme6gkvlG0wm8ze3m+NT62rHzp3PuaIb8nb/5Vy+px6yz s4mqkQw0dhbkIkwZY+x7HqQYYblfgpU3vgSlLIovXh1ZeI2QvTtpcTfDqI438+JXm+XF CLSxI+cXewVDOyUe0LbXQfDlPHoTiLsEa/81rK4f7ftUl005GxTRmxpaSJhBbgL30Ar4 76nhTH+1WI+0cmmu+rUG3b18anVvvv550IE4WrTqKJvw3Z/UYNIz6gdS1QCSNj+fHxRN +YSocy38qvfRuMJogfzph88L4M3/YmMMO3hd1kqVJcqd5i97FuPIGDMDM3P/Zdyt9Hkk Z1qA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWfNJKIO0NeMm7QijHFJrPj6AlTBNowBp8cxWFaYdW/KOFRT+e8 ZHMpR10l7SOl0Uzq8LOLkuE= X-Google-Smtp-Source: APXvYqyFgRzJGYtaR2fXsE4ubERYS688etgg8rTtHekGW2SthWlI6xlNEB7RyItbSDff8pk4CiaflQ== X-Received: by 2002:aca:e106:: with SMTP id y6mr8270123oig.77.1560701081199; Sun, 16 Jun 2019 09:04:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:76d3:: with SMTP id p19ls1278136otl.0.gmail; Sun, 16 Jun 2019 09:04:40 -0700 (PDT) X-Received: by 2002:a9d:1909:: with SMTP id j9mr6041613ota.139.1560701080575; Sun, 16 Jun 2019 09:04:40 -0700 (PDT) Date: Sun, 16 Jun 2019 09:04:39 -0700 (PDT) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <2b7b0d66-4787-4fad-9ee4-7a0bd29faab8@googlegroups.com> In-Reply-To: <304eddc1-2dda-40b6-b512-44b826e2586b@googlegroups.com> References: <31a5586c-c66a-4d66-a384-199d9d453a3b@googlegroups.com> <304eddc1-2dda-40b6-b512-44b826e2586b@googlegroups.com> Subject: [HoTT] Re: A unifying cartesian cubical type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1343_479336571.1560701079879" 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_1343_479336571.1560701079879 Content-Type: multipart/alternative; boundary="----=_Part_1344_663595420.1560701079879" ------=_Part_1344_663595420.1560701079879 Content-Type: text/plain; charset="UTF-8" With Andrew Swan we have now worked out a categorical presentation of our generalized notion of fibrations for cartesian cubical sets. We have also proved that Sattler's model structure theorem applies. For details see: https://github.com/mortberg/gen-cart/blob/master/modelstructure.pdf A special case of our result is a model structure on cartesian cubical sets that does not require that the diagonal map on the interval is a cofibration (i.e. "diagonal cofibrations"). We hence obtain the Sattler model structure on De Morgan and distributive lattice cubical sets as a special case when the cube category has connections. Furthermore, we also obtain the model structure on cartesian cubical sets sketched by Coquand ( https://groups.google.com/forum/#!msg/homotopytypetheory/RQkLWZ_83kQ/tAyb3zYTBQAJ) and more recently spelled out in detail by Awodey ( https://github.com/awodey/math/blob/master/QMS/qms.pdf) when we add the assumption of diagonal cofibrations. We have also formalized the cubical model based on generalized fibrations in the Orton-Pitts style using Agda: https://github.com/mortberg/gen-cart/tree/master/agda The formalization contains the standard type formers of cubical type theory (Pi, Sigma, Path, Id, Glue and univalence). We have not yet formalized the LOPS universe construction as this requires a special branch of Agda that we're waiting for to get merged into master, but we don't expect any problems with this as LOPS applies to cartesian cubical sets as exponentiating by the interval has a right adjoint. Furthermore, the LOPS construction has already been formalized for cartesian cubical sets in ABCFHL (https://github.com/dlicata335/cart-cube). We have also formalized the construction of both of the two factorization systems using Andrew's W-types with reductions (https://arxiv.org/abs/1802.07588). Comments are very welcome! -- Anders, Evan and Andrew -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/2b7b0d66-4787-4fad-9ee4-7a0bd29faab8%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_1344_663595420.1560701079879 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
With Andrew Swan we have now worked out = a categorical=20 presentation of our generalized notion of fibrations for cartesian=20 cubical sets. We have also proved that Sattler's model structure theore= m applies. For details see:

https://g= ithub.com/mortberg/gen-cart/blob/master/modelstructure.pdf

A special case of our result is a model structure on cartesian cubical=20 sets that does not require that the diagonal map on the interval is a=20 cofibration (i.e. "diagonal cofibrations"). We hence obtain the S= attler=20 model structure on De Morgan and distributive lattice cubical sets as a=20 special case when the cube category has connections. Furthermore, we=20 also obtain the model structure on cartesian cubical sets sketched by=20 Coquand (https://groups.google.com/forum/#!msg/homotopytypetheory/R= QkLWZ_83kQ/tAyb3zYTBQAJ) and more recently spelled out in detail b= y Awodey (https://github.com/awodey/math/= blob/master/QMS/qms.pdf) when we add the assumption of diagonal cofibra= tions.


We have also formalized the cubical model based on generalized fibrations i= n the Orton-Pitts style using Agda:


The formalization contains the standard type formers of cubical type=20 theory (Pi, Sigma, Path, Id, Glue and univalence). We have not yet=20 formalized the LOPS universe construction as this requires a special=20 branch of Agda that we're waiting for to get merged into master, but we= =20 don't expect any problems with this as LOPS applies to cartesian cubica= l sets as exponentiating by the interval has a right adjoint.=20 Furthermore, the LOPS construction has already been formalized for=20 cartesian cubical sets in ABCFHL (https://github.com/dlicata3= 35/cart-cube). We have also formalized the construction of both of the = two factorization systems using Andrew's W-types with reductions (https://arxiv.org/abs/1802.07588).=

Comments are very welcome!
--
Anders, Evan and Andrew

--
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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/2b7b0d66-4787-4fad-9ee4-7a0bd29faab8%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_1344_663595420.1560701079879-- ------=_Part_1343_479336571.1560701079879--