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 9523fe88 for ; Sat, 16 Feb 2019 00:14:59 +0000 (UTC) Received: by mail-it1-x139.google.com with SMTP id v125sf11689537itc.4 for ; Fri, 15 Feb 2019 16:14:59 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550276098; cv=pass; d=google.com; s=arc-20160816; b=uHNSp+4tcB8odvoWvHov5aIb3Dgyz2T1NshQu/FQ267B/NCFoUfSqfdC0CulQqLYWi xMMoOSWLikjCzqHDlsTuR2mOM4nM96PSn6gxy3eQr5NGqqXSBfl9gXjFinqwGYi/fNl5 FyPP9fQTWbt8wWnwU/QJLWMa4ivtExvtINAm/QeT1L0pDNhFhyAZYzMdGp2KYnyFhZsl 0A4RB+tVB8935Tby0nQPD2fTBSXVuj54LkG3c3qSFObNZ8nE8oZseJTHNzY7pvwqr/vj Ms9C6NQzXf92GGlLGmMrj9f76r20sI2nAcyp8lx0BMp6M3xIUZA4SOQ2KfxEqpLKIRPO mW4g== 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:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:dkim-signature; bh=KarKcrus3JVLTi2QHNrAEEGauADEQmeBRkwmURzbexo=; b=gXbW5/blwiM19vV46r3dbxYIB4i1I2SU3vapYyuzoS8R7l+B2pebaXAPrS0C/IHmMp lmBW/GUKvJMFRuKgEE+uKleex0HpCbvfKh26VVgD0Rfk9CdmeSFeHOAH/1c3waTGNpYF CVh/kE23uo6cauJGWwnuYvQkkdG4PpeO3uo2QZF1+NTTwsHS5oiRY4kW3tDIMBpg95ij pYeU4ZFyCoByFPuA7R7YyaDJt41EXt2f/qQht9p/OTOcPKKpMQbdkizz7FKxugsWz2lx Y+yOn7fSAkW28ZLH5XiOjnO+166P397YnTME+LDBZJlKuqdui+N/DB+VhM7tVU0voSaq CSFQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=OBM1SfcT; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::12b as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=KarKcrus3JVLTi2QHNrAEEGauADEQmeBRkwmURzbexo=; b=gcVRtVWIYEHodUGlYUuQjVri0/5iZB8IqfhunU/prjhy6bdT6VJE2S1DTP4i2T2f08 d/06QM3uiA/k4gNPf+icGIMAdhfqDVWAP9nj/ADuAn7LYRDUIubqbRChVCj36cCzDLNV uO70QXyw992xo0SuqViH6ANpeWb7FGQp7YAXIaO26wDhnvSkL7c0vrK8xdfaav17jhO4 +j5WW1X1IK1M8v58qk8fQJqUhSIB3ETt33xZ9iShLPAmeEkoeJMjoMzqaT0GS2TFM/+N fsAwYY79ybdA1KC/FbwHM1x8CbrySHEQpzbkkYNLGbM/JVoGk6DMW9xFHmrrcZNXV/u+ E9Vw== 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:subject:from:in-reply-to :date:cc:content-transfer-encoding:message-id:references: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=KarKcrus3JVLTi2QHNrAEEGauADEQmeBRkwmURzbexo=; b=sm5xjVm6HuZUdAB4J1s/s9tHPhYTZP2fls627KbVi+swnU+ADpNxNlY6zFJfFW1MSl zmCG8SP9LyWWEtBvCW0K9xKsKO3sU3+b7NRYk9vrNwMIswNboin6iOaqxvaQjwwiKoVy Kcndyxg5FRFbq36rU3zSNRtZVqsB9Im4O3wVTTpxbwq1xQtvRGEHctfS7sJLJc8VF9fa 5Gg8kezgMtao+4Q3iBevZbEOqZv2x/I8uQF7LBuocOyX0Mvi9bNcX6E06Rb97m4e7tKC XrsSQ4IeRIzWq8Rr9w+di8JBeSpg7cqouMIYAfjPI08FCTy2zRsjseWmlZc3Kp9tc6W5 psWQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZzMgN5kFdSGWOl4svDMXfADNM59vv13hfV11A8vxoFrNR6Y86S qp1mI4XAMyWlGrY7HMZUf4A= X-Google-Smtp-Source: AHgI3IaTLPUrsBUWpLVMp1594Rt7xXyOQ77gOxy1doB+PhIZknRQIFDj42TClTymbwFOVNJwrxmqkw== X-Received: by 2002:a02:6248:: with SMTP id d69mr60818jac.1.1550276098750; Fri, 15 Feb 2019 16:14:58 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:694d:: with SMTP id e74ls2144166itc.4.canary-gmail; Fri, 15 Feb 2019 16:14:58 -0800 (PST) X-Received: by 2002:a24:4341:: with SMTP id s62mr7148967itb.17.1550276098272; Fri, 15 Feb 2019 16:14:58 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550276098; cv=none; d=google.com; s=arc-20160816; b=lgraEO5eePVJA+V+PXUIb3eJeUDFmuz85MrqcWlCOZ5rsARjSUp/9/FL8384Df71DW 2hHeB1Y9ANoea5m7lpMt6IrH0tzkHBbU5HyBd7HKm9s+SxWdlcTAlW5tgXtw8Ktzhxcs HKg4eLYo+Q6w0mdnKvMtFUXABcpHVWLUhQoiPXWHNs9tFqs/0dLuX5fVTRJcuv2tcutH NqXknd9M94fgCvtNVwmMc1CJ6DzWo4UvDa34t+cMhDGsQF4xfbfL04RJZpcfFRIyh8ue u41HyLY6dYHxJePDflca8URxPJQI1UPgG8vHqPSXa93zIVzrmlEWLNcclvgbMQIAsKYF nSgw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=h5II4tvzPiJHP8UkeBPBJhg+Rf4X768JVo2KpFNlp04=; b=mzByNyWH3rz1TD+eLGderVvV1mf303t8YNi3UkH/XmosaxUhqVR3ho9d3pkRVpw7po BedwUzLbg5tPXDniZfAeSp7nz53dDi8y22Jzh8IUNxUX37IR9OrNCteVjJVrifYq+tb5 pMumsnwDc2wqeoiuBNiKfkzI/wBO0Tdv682aFkmB14bmijMxknGyuwOyfPFfctOzyd89 tbs05TaUUhXNtMfbxXKu78xdGBlazbGpBivrBhsKTb9mbHPfsLlNGTDWgpGOhn0t5DN7 +ecXJeODnCzD310+WUV0NxlXtit4VJI0i+qS9JFt9ZNiWGaJNGBbjdib1REdUTzormh2 Fkpg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=OBM1SfcT; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::12b as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-it1-x12b.google.com (mail-it1-x12b.google.com. [2607:f8b0:4864:20::12b]) by gmr-mx.google.com with ESMTPS id m141si420381itm.0.2019.02.15.16.14.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 15 Feb 2019 16:14:58 -0800 (PST) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::12b as permitted sender) client-ip=2607:f8b0:4864:20::12b; Received: by mail-it1-x12b.google.com with SMTP id y184so28365067itc.1 for ; Fri, 15 Feb 2019 16:14:58 -0800 (PST) X-Received: by 2002:a24:118e:: with SMTP id 136mr776925itf.175.1550276097945; Fri, 15 Feb 2019 16:14:57 -0800 (PST) Received: from [172.16.15.223] ([65.196.126.174]) by smtp.gmail.com with ESMTPSA id c15sm2906432ioi.66.2019.02.15.16.14.56 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 15 Feb 2019 16:14:57 -0800 (PST) Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: Re: [HoTT] A unifying cartesian cubical type theory From: Steve Awodey In-Reply-To: Date: Fri, 15 Feb 2019 19:14:55 -0500 Cc: =?utf-8?Q?Anders_M=C3=B6rtberg?= , Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> References: To: Michael Shulman X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=OBM1SfcT; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::12b as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.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: , I think the idea is that the model structure is constructed / proved using = ideas from type theory (like univalence), rather than that it is a model of= type theory. But I agree that the terminology is confusing. =20 The methodology is, I think, due to Christian Sattler =E2=80=94 so maybe Sa= ttler model structure is more appropriate? Steve > On Feb 15, 2019, at 7:01 PM, Michael Shulman wrote= : >=20 > 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"? >=20 > On Fri, Feb 15, 2019 at 8:32 AM Anders M=C3=B6rtberg > wrote: >>=20 >> 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). >>=20 >> The observation that the type theoretic model structure on De Morgan cub= ical sets is not equivalent to the one on spaces is simpler than for Cartes= ian 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 n= o reversals), i.e. the "Dedekind" cubes. >>=20 >> -- >> Anders >>=20 >> On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: >>>=20 >>> Thanks. This looks very interesting. >>>=20 >>> Did you think about the corresponding model structure? >>> https://ncatlab.org/nlab/show/type-theoretic+model+structure >>>=20 >>> 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 >>>=20 >>> On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg >>> wrote: >>>>=20 >>>> 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: >>>>=20 >>>> http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf >>>>=20 >>>> 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. >>>>=20 >>>> 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). >>>>=20 >>>> -- >>>> Anders and Evan >>>>=20 >>>> -- >>>> 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. >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 > --=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= 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.