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.0 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-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 003395f2 for ; Mon, 18 Feb 2019 14:05:58 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id 32sf15190043ots.15 for ; Mon, 18 Feb 2019 06:05:57 -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=T0tV2atguxvQqXgxiL4tS+cwnA+DEFVMVhH5Wo40orE=; b=rh15Jc6fWQvwS9DJu5iQJyuPCQGbb9t2OIkVwtJNN3PpFEDfyexlpVy3VVDwDVnYqg 4puZmtHZr2+nk8bBpDWHnfkXh+WY7COmSZsvKwpP9Pe+OBo4dXADqp3EL3Ztn94HP6Bl rMQiENzGMGg0cWGoyx+cNOZmZCnlfUyWcxcoaz+/YJ2Zs9yEQG9CMRDHj8/QszRaN651 XsnFt8A+NnjWy5ak16aUnmEYh3i1wn/h8NHT0CrE9hz6r29BY1r/dZ5ATsTEvin9iFj4 S0cEu5c9U3EjVoXrCMRLmOzRJjoFHO4RnJCFvkcT9nKgi4INC0RxLHMKLpL816j3Z2pj UuEA== 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=T0tV2atguxvQqXgxiL4tS+cwnA+DEFVMVhH5Wo40orE=; b=lHUXGBvVyp48akVmhiWjN4NSntBvWvxT7+0XAYyviQrMOUf+R4ZobQA9JDpKYUDYNk nDfYjy6Xsv7TdHCd5l49Snj4VY5NGzXeeM/8NaIQQ7qu0p9xRC1WLLJGrRNc5cUkmD8+ B+RHTcFGTwkWOuN8mEj9+UtEsN9wTt6f3IpcvyKGuSP3wX98GG+iuObsdF8Sq+D2oNHn i0rYdw1nJIjoUREMnlY8XFfBBccp0hRi80FwfX32volyB7tz9SecqAcR2qRy3hmAc6Da 0D4p5Yim/l8EaR+SX+nVuFFqA30eiCqeMeIqDsywt9l29wZnzbX98VLwOwDQ5iOWrRcl NHqw== 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=T0tV2atguxvQqXgxiL4tS+cwnA+DEFVMVhH5Wo40orE=; b=HBUvlkrzE3b2XySXBX09EUqeKJQNnfhtcd/dHGPneZVCEYuk12064/pWqgEmeS3z/m MDDo2TtIUDeqyzBbtWw8lrcdB1s/J0oFBXqJlG4uE8rwgFIO52S8sQQewdVH/wO1CDQy GW8uvz0/NhKUkBWxSwfCbQHde6lco7gqLkOjmj3DaeLBfqEPOQZPIuyVxyqOfklkuz7O i3s6jUDGI9MT3K3Y3wylNe2zhwlqNRXy/TAOyByzT2afk3SHNeOtcsUd6pU6CrVEzQUo Z3qJTmrHqbAMrf5Tfj8DVvoDCNxtlohFA7IJqbkatRQIj61RcexB1YH/Q7lLaFpbKrRm 4KTA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYuFO1yyBxNNGX2BYfeWngT0lZcrlwG6DSf5OVMYtQl+THyhgNQ hsSuUVXb80kwklz3v+x7P6k= X-Google-Smtp-Source: AHgI3Ib2HlH88ih9LS+RsY9QMBUIN4hfviDpwXUluBG+l3p2Sg3QBUvL2gxRVWnAaqj70u9pO/H/7w== X-Received: by 2002:aca:cf4f:: with SMTP id f76mr246969oig.7.1550498756182; Mon, 18 Feb 2019 06:05:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:bbd6:: with SMTP id l205ls7823361oif.3.gmail; Mon, 18 Feb 2019 06:05:55 -0800 (PST) X-Received: by 2002:aca:5592:: with SMTP id j140mr250586oib.5.1550498755174; Mon, 18 Feb 2019 06:05:55 -0800 (PST) Date: Mon, 18 Feb 2019 06:05:54 -0800 (PST) From: Andrew Swan To: Homotopy Type Theory Message-Id: <31a5586c-c66a-4d66-a384-199d9d453a3b@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: A unifying cartesian cubical type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_591_1851926280.1550498754369" X-Original-Sender: wakelin.swan@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_591_1851926280.1550498754369 Content-Type: multipart/alternative; boundary="----=_Part_592_1770209418.1550498754370" ------=_Part_592_1770209418.1550498754370 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I decided to have a go at translating the ideas over to lifting problems=20 and model structures. Dan's remarks were quite helpful and possibly some of= =20 this is a rephrasing of those ideas. We have an interval object I, and write d0 and d1 for the endpoint=20 inclusions 1 -> I. We want to ensure in any case that for i =3D 0,1 di has= =20 the enriched/fibred/internal left lifting property against every fibration.= =20 That is, for every object B, we want that the maps (1, di) : B -> B x I are= =20 trivial cofibrations. Now if the (trivial) (co)fibrations we defined are=20 going to form part of a model structure, we will need that for any map r := =20 B -> I, the map (1, r) : B -> B x I is a weak equivalence. This is because= =20 the projection B x I -> B is a weak equivalence by applying 3-for-2 and=20 using that (1, d0) is a trivial cofibration, and then applying 3-for-2=20 again the other way, it follows that (1, r) is a weak equivalence. Therefore when we define fibrations, we want to ensure that we do so in a= =20 way that guarantees (1, r) : B -> B x I is a weak equivalence. If I has=20 connections, then it would be easier, but they are not present in cartesian= =20 cubical sets, so we look for some other way. One way to do this is to choose the generating trivial cofibrations so that= =20 every map (1, r) is a trivial cofibration. For some other arguments to=20 work, we include not just these maps, but close under pushout product with= =20 cofibrations. Therefore we take the generating trivial cofibrations to be= =20 every map generated as follows: Given a map r : B -> I, and a cofibration m= =20 : A -> B, we note that m and (1, r) can both be viewed as maps in the slice= =20 category C/B. We construct the pushout product of (1, r) and m in the slice= =20 category, and take this to be a generating trivial cofibration. This gives= =20 the ABCFHL definition of fibration. However, this has the disadvantage that as a special case we have made the= =20 map I -> I x I a trivial cofibration, so if we want this to be part of a=20 model structure we also need it to be a cofibration. This means we can't=20 take the face lattice to be the (generating) cofibrations. Therefore we need a way to choose the trivial cofibrations that makes every= =20 map (1, r) : B -> B x I a weak equivalence without adding any new=20 cofibrations. We again work in the slice category over B. Since we are now= =20 working in the slice category, the terminal object 1, is the identity on B,= =20 and we have a cofibrant subobject A of 1, and a map r : 1 -> I. We take the= =20 mapping cylinder factorisation of r to get 1 -> T -> I. One can show that= =20 the map 1 -> T is a cofibration (assuming endpoint inclusions are disjoint= =20 and both cofibrations, and cofibrations are closed under pullback). Hence= =20 if we make 1 -> T a trivial cofibration, it won't add any new cofibrations.= =20 Moreover making 1 -> T a weak equivalence promises to be a reasonable=20 substitute for making r a weak equivalence, because the map T -> I should= =20 also be weak equivalence in any case. Now, as before we also close under=20 pushout product with m, again computed in the slice category over B. Unfolding the definition of mapping cylinder, we get a concrete description= =20 of T. It is the pushout of two copies of I, along the maps d0 : 1 -> I and= =20 r : 1 -> I, making a "T" shape where the end of one interval is joined to= =20 the other at point r. We can also illustrate what the pushout product with= =20 a cofibration looks like, using the boundary inclusion 2 -> I as an=20 example: The codomain is the product T x I and the domain is the subobject= =20 consisting of two copies of T on each end of the cylinder together with a= =20 line connecting the bases of the Ts. It's a little tricky to show the=20 resulting definition of fibration follows from Anders and Evan's=20 definition, but I think it works, by using their observation that they do= =20 have Kan composition in the usual sense for open boxes (pushout products of= =20 cofibrations and endpoint inclusions). It seems reasonable to conjecture then that the Mortberg-Cavallo definition= =20 of fibration and trivial fibration form part of a model structure, and=20 moreover we might also conjecture that if we define fibration to be "right= =20 lifting property against open box inclusion" and cofibration to be given by= =20 the face lattice it does not extend to a model structure on cartesian=20 cubical sets. Best, Andrew On Thursday, 14 February 2019 20:05:07 UTC+1, Anders M=C3=B6rtberg wrote: > > Evan Cavallo and I have worked out a new cartesian cubical type theory=20 > that generalizes the existing work on cubical type theories and models=20 > 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=20 > depends neither on diagonal cofibrations nor on connections or=20 > reversals. In the presence of these additional structures, our notion=20 > of fibration coincides with that of the existing cartesian and De=20 > Morgan cubical set models. This work can therefore be seen as a=20 > generalization of the existing models of univalent type theory which=20 > also clarifies the connection between them.=20 > > The key idea is to weaken the notion of fibration from the cartesian=20 > Kan operations com^r->s so that they are not strictly the identity=20 > when r=3Ds. Instead we introduce weak cartesian Kan operations that are= =20 > only the identity function up to a path when r=3Ds. Semantically this=20 > should correspond to a weaker form of a lifting condition where the=20 > lifting only satisfies some of the eqations up to homotopy. We verify=20 > in the note that this weaker notion of fibration is closed under the=20 > type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue,=20 > U) so that we get a model of univalent type theory. We also verify=20 > that the circle works and we don't expect any substantial problems=20 > with extending it to more complicated HITs (like pushouts).=20 > > --=20 > Anders and Evan=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_592_1770209418.1550498754370 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I decided to have a go at translating the ideas over to li= fting problems and model structures. Dan's remarks were quite helpful a= nd possibly some of this is a rephrasing of those ideas.

We have an interval object I, and write d0 and d1 for the endpoint inclusi= ons 1 -> I. We want to ensure in any case that for i =3D 0,1 di has the = enriched/fibred/internal left lifting property against every fibration. Tha= t is, for every object B, we want that the maps (1, di) : B -> B x I are= trivial cofibrations. Now if the (trivial) (co)fibrations we defined are g= oing to form part of a model structure, we will need that for any map r : B= -> I, the map (1, r) : B -> B x I is a weak equivalence. This is bec= ause the projection B x I -> B is a weak equivalence by applying 3-for-2= and using that (1, d0) is a trivial cofibration, and then applying 3-for-2= again the other way, it follows that (1, r) is a weak equivalence.

Therefore when we define fibrations, we want to ensure th= at we do so in a way that guarantees (1, r) : B -> B x I is a weak equiv= alence. If I has connections, then it would be easier, but they are not pre= sent in cartesian cubical sets, so we look for some other way.

One w= ay to do this is to choose the generating trivial cofibrations so that ever= y map (1, r) is a trivial cofibration. For some other arguments to work, we= include not just these maps, but close under pushout product with cofibrat= ions. Therefore we take the generating trivial cofibrations to be every map= generated as follows: Given a map r : B -> I, and a cofibration m : A -= > B, we note that m and (1, r) can both be viewed as maps in the slice c= ategory C/B. We construct the pushout product of (1, r) and m in the slice = category, and take this to be a generating trivial cofibration. This gives = the ABCFHL definition of fibration.

However, this = has the disadvantage that as a special case we have made the map I -> I = x I a trivial cofibration, so if we want this to be part of a model structu= re we also need it to be a cofibration. This means we can't take the fa= ce lattice to be the (generating) cofibrations.

Th= erefore we need a way to choose the trivial cofibrations that makes every m= ap (1, r) : B -> B x I a weak equivalence without adding any new cofibra= tions. We again work in the slice category over B. Since we are now working= in the slice category, the terminal object 1, is the identity on B, and we= have a cofibrant subobject A of 1, and a map r : 1 -> I. We take the ma= pping cylinder factorisation of r to get 1 -> T -> I. One can show th= at the map 1 -> T is a cofibration (assuming endpoint inclusions are dis= joint and both cofibrations, and cofibrations are closed under pullback). H= ence if we make 1 -> T a trivial cofibration, it won't add any new c= ofibrations. Moreover making 1 -> T a weak equivalence promises to be a = reasonable substitute for making r a weak equivalence, because the map T -&= gt; I should also be weak equivalence in any case. Now, as before we also c= lose under pushout product with m, again computed in the slice category ove= r B.

Unfolding the definition of mapping cylinder,= we get a concrete description of T. It is the pushout of two copies of I, = along the maps d0 : 1 -> I and r : 1 -> I, making a "T" sha= pe where the end of one interval is joined to the other at point r. We can = also illustrate what the pushout product with a cofibration looks like, usi= ng the boundary inclusion 2 -> I as an example: The codomain is the prod= uct T x I and the domain is the subobject consisting of two copies of T on = each end of the cylinder together with a line connecting the bases of the T= s. It's a little tricky to show the resulting definition of fibration f= ollows from Anders and Evan's definition, but I think it works, by usin= g their observation that they do have Kan composition in the usual sense fo= r open boxes (pushout products of cofibrations and endpoint inclusions).

It seems reasonable to conjecture then that the Mort= berg-Cavallo definition of fibration and trivial fibration form part of a m= odel structure, and moreover we might also conjecture that if we define fib= ration to be "right lifting property against open box inclusion" = and cofibration to be given by the face lattice it does not extend to a mod= el structure on cartesian cubical sets.


=
Best,
Andrew



On Thursday, 1= 4 February 2019 20:05:07 UTC+1, Anders M=C3=B6rtberg wrote:
Evan Cavallo and I have worked out a new cart= esian 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/u= nifying-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=3Ds. Instead we introduce weak cartesian Kan operations that are
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).

--
Anders and Evan

--
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_592_1770209418.1550498754370-- ------=_Part_591_1851926280.1550498754369--