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-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 22488745 for ; Mon, 18 Feb 2019 15:31:43 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id a1sf14696709otl.9 for ; Mon, 18 Feb 2019 07:31:43 -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=dupVy8kmf1YVgTkMCGGywIs3zPJHNV4+I4I2gVYNUE4=; b=izQBbTJdxXwAs0LxF3qJjRbnelWDOBGOwgOG1eBnCT8ISxcYgSR8kh/ztPv+WCb5OL EnxkphLiw30ygC41c42vKLfhW/yv/NeVl2eeqHsWiOdNh7s8MuUcxhNjYjj6icAdDB4+ RvnL60/GcfNQ4I/AHZGUhbW3xHnhsJQzHOpHesMZ1Hu+h9K7/NmA3QUnLP2VrpxpWtA+ ed8P7dFcTzHq3kXosmhk+DlXjfvgNfleh9ODhNSpFbtHB/QQ85xCRA+jxvXF0xgE9yET iebhuRnvigMl9YklCp4JBK1Ol45vMPnWbvhSm3zEBP1zRyk/6gcOuqt5pNRgpHjZoKs6 SwWg== 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=dupVy8kmf1YVgTkMCGGywIs3zPJHNV4+I4I2gVYNUE4=; b=rRrAa+R2U0KU2e5e2dYXQpbsAytxe/CfK5TXEx+H8iJO+jC3OgbX8tyoWlR8Jwj77n XzbgAcb8UK8W0Zr+7bI1HM4LNz4ulG4Z2KoiRZkltWa7HAhYZ39C5WuS9qu+tqkTNDLl 8TP5agU2XcQItXpxdVdt9MPtwlAAM/q/AvP4/KqCoylPTZ+9NUw3ncDIIudy5x0N2K5z D6JSpgYHqsreSXtCQCjrX18UUc0rhiOrMBRxR/j25J6d/wi1hAzC4YW70u9bxJ6qUSQg SmZfMSN5ZTkKuj6pe49+YTPiQKzJ6rDfBqO/WLC74q0GhyR7A24iOG4EiM92WHhJLydC 1B5w== 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=dupVy8kmf1YVgTkMCGGywIs3zPJHNV4+I4I2gVYNUE4=; b=ExfXH2w76welwCgNYbrdGtpqCP+liCPt7fk23y/315sgMMSpcQlIez8e7mi2dbJ7ox lP2/g5aUlgCYL8eOXLkwOqV0wQ1p1PsPxvmyD1eqjarZ5fLZonVrMymwJh+1PLmwumM4 ck5jhOMvCwAsYMhf1jc7n/Q66GdFQ2T0v1gm7HGvQMDuyrDunWEd0+d/BwPVajkjtPQJ UAq7E4GfjMir7SR3jU1MOiuMe//eO61vthg0xXYXLs0OPqxmqpyb22BUnS8FcEPoA5+h TOV2GC/dVkHX+l+flfEqIm2xezarQnIjg5lTvxucjjEn8PMci5l3/vci/ArdjHj+ocaR c30A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaOAVmF4J/F6QCZZWOtqSDgezrphsPy5rGxzHZLmyIB1o8GdY88 z7YWHXxVQpOGuJHZMwITG1Q= X-Google-Smtp-Source: AHgI3IbO/WV/pJeVPFGejFGPgn7GGZ3nstBnnb2MB0PlSk49BloWPS8MLbABi1xw7iwp+nne1qiukg== X-Received: by 2002:aca:eb83:: with SMTP id j125mr357oih.1.1550503902201; Mon, 18 Feb 2019 07:31:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3d54:: with SMTP id k81ls8297112oia.1.gmail; Mon, 18 Feb 2019 07:31:41 -0800 (PST) X-Received: by 2002:a54:4d86:: with SMTP id y6mr456oix.0.1550503901542; Mon, 18 Feb 2019 07:31:41 -0800 (PST) Date: Mon, 18 Feb 2019 07:31:40 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <304eddc1-2dda-40b6-b512-44b826e2586b@googlegroups.com> In-Reply-To: <31a5586c-c66a-4d66-a384-199d9d453a3b@googlegroups.com> References: <31a5586c-c66a-4d66-a384-199d9d453a3b@googlegroups.com> Subject: [HoTT] Re: A unifying cartesian cubical type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_659_1103914173.1550503900568" 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_659_1103914173.1550503900568 Content-Type: multipart/alternative; boundary="----=_Part_660_1478811117.1550503900568" ------=_Part_660_1478811117.1550503900568 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks Dan and Andrew for analyzing our work further!=20 I find Dan's reformulation of our Kan condition quite illuminating:=20 A : I =E2=86=92 Set has Kan composition iff =CE=A0 r:I, the map (=CE= =BB f =E2=86=92 f r) : (=CE=A0=20 (x : I) =E2=86=92 A x) =E2=86=92 (A r) is an equivalence=20 My intuition is that this says that A is fibrant iff for any r : I the type= =20 A r can be extended to all of I in a uniform way. I believe that we can reformulate the Kan condition we had in CCHM as: A : I =E2=86=92 Set has Kan composition iff the map (=CE=BB f =E2=86= =92 f 0) : (=CE=A0 (x : I)=20 =E2=86=92 A x) =E2=86=92 (A 0) is an equivalence=20 In the presence of a meet connection these two formulations are path-equal= =20 by moving along "i /\ r" (this is what motivates the use of connections in= =20 CCHM).=20 What our note shows is that this natural generalization of CCHM is closed= =20 under all of the cubical type formers and hence form a model of univalent= =20 type theory even in the absence of connections. In particular it is not=20 necessary to further require the strict fibers as in AFH/ABCFHL when=20 generalizing CCHM. This is what lets us drop the assumption that the=20 diagonal I -> I x I is a cofibration (what we referred to as "diagonal=20 cofibrations" above) in order to construct univalent fibrant universes. I haven't yet had time to analyze Andrew's definition, but if it works then= =20 I would be very interested in knowing if the Sattler model structure=20 construction works. If I understand Christian's work correctly the=20 construction of the WFS's require very few assumptions and the 2-out-of-3= =20 property relies on the equivalence extension property which follows from=20 the existence of fibrant Glue types (which is in our note). -- Anders On Monday, February 18, 2019 at 9:05:54 AM UTC-5, Andrew Swan wrote: > > 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 ha= s=20 > the enriched/fibred/internal left lifting property against every fibratio= n.=20 > That is, for every object B, we want that the maps (1, di) : B -> B x I a= re=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 becaus= e=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 cartesi= an=20 > cubical sets, so we look for some other way. > > One way to do this is to choose the generating trivial cofibrations so=20 > that 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 wit= h=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 sli= ce=20 > category C/B. We construct the pushout product of (1, r) and m in the sli= ce=20 > category, and take this to be a generating trivial cofibration. This give= s=20 > the ABCFHL definition of fibration. > > However, this has the disadvantage that as a special case we have made th= e=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=20 > every 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 no= w=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 t= he=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 disjoin= t=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 cofibration= s.=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=20 > description of T. It is the pushout of two copies of I, along the maps d0= :=20 > 1 -> I and r : 1 -> I, making a "T" shape where the end of one interval i= s=20 > joined to the other at point r. We can also illustrate what the pushout= =20 > product with a cofibration looks like, using the boundary inclusion 2 -> = I=20 > as an example: The codomain is the product T x I and the domain is the=20 > subobject consisting of two copies of T on each end of the cylinder=20 > together with a line connecting the bases of the Ts. It's a little tricky= =20 > to show the resulting definition of fibration follows from Anders and=20 > Evan's definition, but I think it works, by using their observation that= =20 > they do have Kan composition in the usual sense for open boxes (pushout= =20 > products of cofibrations and endpoint inclusions). > > It seems reasonable to conjecture then that the Mortberg-Cavallo=20 > definition of fibration and trivial fibration form part of a model=20 > structure, and moreover we might also conjecture that if we define=20 > fibration to be "right lifting property against open box inclusion" and= =20 > cofibration to be given by the face lattice it does not extend to a model= =20 > structure on cartesian 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_660_1478811117.1550503900568 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks Dan and Andrew for analyzing our work further!=

I find Dan's reformulation of our Kan co= ndition quite illuminating:

=C2=A0 =C2=A0 A : I = =E2=86=92 Set has Kan composition iff=C2=A0=C2=A0 =CE=A0 r:I, the map (=CE= =BB f =E2=86=92 f r) : (=CE=A0 (x : I) =E2=86=92 A x) =E2=86=92 (A r)=C2=A0= =C2=A0=C2=A0 is an equivalence

My intuition is that this says that A is fibrant if= f for any r : I the type A r can be extended to all of I in a uniform way.<= br>

I believe that we can reformulate the Kan cond= ition we had in CCHM as:

=C2=A0 =C2=A0 A : I = =E2=86=92 Set has Kan composition iff=C2=A0=C2=A0 the map (=CE=BB f =E2=86= =92 f 0) : (=CE=A0 (x : I) =E2=86=92 A x) =E2=86=92 (A 0)=C2=A0=C2=A0=C2=A0= is an equivalence

In the presence of a meet connection these two form= ulations are path-equal by moving along "i /\ r" (this is what mo= tivates the use of connections in CCHM).

What= our note shows is that this natural generalization of CCHM is closed under= all of the cubical type formers and hence form a model of univalent type t= heory even in the absence of connections. In particular it is not necessary= to further require the strict fibers as in AFH/ABCFHL when generalizing CC= HM. This is what lets us drop the assumption that the diagonal I -> I x = I is a cofibration (what we referred to as "diagonal cofibrations"= ; above) in order to construct univalent fibrant universes.
<= br>

I haven't yet had time to analyze Andrew&#= 39;s definition, but if it works then I would be very interested in knowing= if the Sattler model structure construction works. If I understand Christi= an's work correctly the construction of the WFS's require very few = assumptions and the 2-out-of-3 property relies on the equivalence extension= property which follows from the existence of fibrant Glue types (which is = in our note).

--
Anders


On Monday, February 18, 2019 at= 9:05:54 AM UTC-5, Andrew Swan wrote:
I decided to have a go at translating the ideas ove= r to lifting problems and model structures. Dan's remarks were quite he= lpful and possibly some of this is a rephrasing of those ideas.

We have an interval object I, and write d0 and d1 for the endpoint = inclusions 1 -> I. We want to ensure in any case that for i =3D 0,1 di h= as the enriched/fibred/internal left lifting property against every fibrati= on. That 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 define= d are going to form part of a model structure, we will need that for any ma= p r : B -> I, the map (1, r) : B -> B x I is a weak equivalence. This= is because 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.<= /div>

Therefore when we define fibrations, we want to en= sure that we do so in a way that guarantees (1, r) : B -> B x I is a wea= k equivalence. If I has connections, then it would be easier, but they are = not present in cartesian cubical sets, so we look for some other way.
One way to do this is to choose the generating trivial cofibrations so th= at every map (1, r) is a trivial cofibration. For some other arguments to w= ork, we include not just these maps, but close under pushout product with c= ofibrations. Therefore we take the generating trivial cofibrations to be ev= ery 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 category 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 = structure we also need it to be a cofibration. This means we can't take= the face lattice to be the (generating) cofibrations.

=
Therefore we need a way to choose the trivial cofibrations that makes = every map (1, r) : B -> B x I a weak equivalence without adding any new = cofibrations. 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 mapping cylinder factorisation of r to get 1 -> T -> I. One can = show that the map 1 -> T is a cofibration (assuming endpoint inclusions = are disjoint and both cofibrations, and cofibrations are closed under pullb= ack). Hence if we make 1 -> T a trivial cofibration, it won't add an= y new cofibrations. Moreover making 1 -> T a weak equivalence promises t= o be a reasonable substitute for making r a weak equivalence, because the m= ap T -> I should also be weak equivalence in any case. Now, as before we= also close under pushout product with m, again computed in the slice categ= ory over B.

Unfolding the definition of mapping cy= linder, 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&qu= ot; shape 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 li= ke, using the boundary inclusion 2 -> I as an example: The codomain is t= he product T x I and the domain is the subobject consisting of two copies o= f T on each end of the cylinder together with a line connecting the bases o= f the Ts. It's a little tricky to show the resulting definition of fibr= ation follows from Anders and Evan's definition, but I think it works, = by using their observation that they do have Kan composition in the usual s= ense for open boxes (pushout products of cofibrations and endpoint inclusio= ns).

It seems reasonable to conjecture then that t= he Mortberg-Cavallo definition of fibration and trivial fibration form part= of a model structure, and moreover we might also conjecture that if we def= ine fibration to be "right lifting property against open box inclusion= " and cofibration to be given by the face lattice it does not extend t= o a model structure on cartesian cubical sets.

Best,
Andrew



On Thur= sday, 14 February 2019 20:05:07 UTC+1, Anders M=C3=B6rtberg wrote:Evan Cavallo and I have worked out a new ca= rtesian 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_660_1478811117.1550503900568-- ------=_Part_659_1103914173.1550503900568--