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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 52a524ac for ; Fri, 15 Feb 2019 15:38:06 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id r22sf2791031otk.1 for ; Fri, 15 Feb 2019 07:38:05 -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=br1BCkKK9nlm8urwNrnjTDoZrP0cDfY38qnaVoZRVQs=; b=VRNICVX1K/oXp+uJgRdIWRLDYSZEJdZdUq7NVp35jJierswiBoFmISbcsnKB+ZV3kz RvqwqFyE+IbiMZKc2ZEAJepSZaJI0G5IN9Yy7R3r1etu/3+Sb9Sugs9RCvtpcdzyJJGy y2KIPIyvYxKqwMY8KBW11AO+7q4U5dQ5ue+e9czsrW0bLZTdFg6zYfEEusZBMUgd+q/V /8aWqhjiZ4mJHWVfvwt8ahRw6bXxxZ10GUfgwVYygJBR9xk1JJ7pz3wJXhDqJtgThHjS /C9qbqK+UALvSzkuq+JE4wUIyc/aVnP8hfz70CLfUCfWDx4WlIyGY5LmutLOaBhPJ+dO eD0w== 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=br1BCkKK9nlm8urwNrnjTDoZrP0cDfY38qnaVoZRVQs=; b=Rz+uRB6bOctvVmqZxYBpVNat85xb1YBPwPjug4k6yu4AZZI0SNvs2/0jV6rA8LQEo3 tJsQR0rGbpgSOOtU0dwdkWOrdiKGs+b/Kkha9OVDu5DK3TCNKFNMt4B7oF4hDJAEAwVO 85J5LuGSDALtrpYbutSmJE+hQARasMiCaYg2g8vSufZlr8ftDUmnfgpputoxxgj9OIGy mOwrReHf9FxOSo+/1vzypZ3hTJVOqk2QyfSJsu47tz124f5wvqfk/9fHGH03oToa6dZy rEOcYooqzVlwo/4ztHrJBT0NIQ6gxcysfYz2JmMrGZVnwfovcyvHQ7w6cxzu4+vrJ75p q9CA== 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=br1BCkKK9nlm8urwNrnjTDoZrP0cDfY38qnaVoZRVQs=; b=ZqFvCBRKEzn1iLD/mCHvVwbHNxW22XTZFDNeEDWZ1sW7tF33upoA4pBDSvoVTsrKKI Xr1jnCffQfFoLBqs+uVzS4JsLmHY3bU88AQagdVaVJDym2io9FfhPjoQ90sVa0tTS3Va Ce84THgt/8AzLERgY+fcda0EXcLp/4OhR1IxTsRzUhIKK5S1RGnJZPKrjIYpcmvFHiFR NIJFEQ7mtp+5ipmei3uewF5Vy4B/4Nff1DknZE0eirPROPbj44OMu8ajx1ya8WVxvZgr xQ9Cgay0/jXdc1r3MD7REHJlYVf28pJih3NmGxymgDMWpdlw38JpHRQFL8aOL3zohUy0 Wbmw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZDPzO71sPonx/H3uVTGWJ+Ar/zYhJ7MsJTTW7UlqF3eDhS0eNi fMLC8pxWDVRGwzf2jvz6vUw= X-Google-Smtp-Source: AHgI3IZjqKI+I8PAeQzmUb5adjVL0xQ1DQ2MYdI1CRoGdVN9gVvYXCf31vwXOV1hd8Yj4hPg27FayQ== X-Received: by 2002:a9d:3476:: with SMTP id v109mr100682otb.7.1550245084976; Fri, 15 Feb 2019 07:38:04 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4605:: with SMTP id p5ls3683572oip.0.gmail; Fri, 15 Feb 2019 07:38:04 -0800 (PST) X-Received: by 2002:aca:df55:: with SMTP id w82mr99126oig.6.1550245084365; Fri, 15 Feb 2019 07:38:04 -0800 (PST) Date: Fri, 15 Feb 2019 07:38:03 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: [HoTT] A unifying cartesian cubical type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_389_1458641519.1550245083753" 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_389_1458641519.1550245083753 Content-Type: multipart/alternative; boundary="----=_Part_390_1830799272.1550245083753" ------=_Part_390_1830799272.1550245083753 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thursday, February 14, 2019 at 3:06:29 PM UTC-5, Andrew Pitts wrote: > > On Thu, 14 Feb 2019 at 19:05, Anders Mortberg > wrote:=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.=20 > > I was interested to read this, because I too use that weakened form=20 > of fibration in some work attempting to get a model of univalence=20 > based only on composition of paths rather than more general Kan=20 > filling operations =E2=80=94 so far unpublished, because I can't quite se= e how=20 > to get univalent universes to work (but seem frustratingly close to=20 > it).=20 > > Very interesting that you also considered this form of weakened fibrations!= =20 I also thought a bit about basing things on a binary composition operation,= =20 but I never could get it to work. I managed to convince myself some year=20 ago that in the presence of connections and reversals (potentially with=20 Boolean structure) homogeneous composition (hcomp^0->1) is equivalent to=20 binary composition, but without this structure on the interval I don't=20 really see what to do. But on the other hand, if you don't have connections= =20 then I don't think you need the fibrations to lift against arbitrary=20 subtubes but rather only open boxes in the sense of BCH... Anyway, the univalent universes (in particular fibrancy of Glue types) is= =20 by far the hardest thing in our note (as seems to always be the case). The= =20 way we do it is an adaptation of what we did back in CCHM, but because of= =20 the weakness we have to do additional corrections in the construction which= =20 makes it quite a bit longer. =20 Anyway, what I wanted to say is that perhaps one should call these=20 > things "Dold fibrations" by analogy with the classic notion of Dold=20 > fibration in topological spaces=20 > ?=20 > > Andy=20 > Thanks for the pointer! I didn't know about them and will have to think a= =20 bit whether what we have could be seen as a cubical variation of them.=20 -- Anders =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_390_1830799272.1550245083753 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thursday, February 14, 2019 at 3:06:29 PM UTC-5, Andrew= Pitts wrote:
On Thu, 14 Feb 20= 19 at 19:05, Anders Mortberg <andersm...@gmail.com> wrote:
> The key idea is to weaken the notion of fibration from the cartesi= an
> Kan operations com^r->s so that they are not strictly the ident= ity
> when r=3Ds. Instead we introduce weak cartesian Kan operations tha= t are
> only the identity function up to a path when r=3Ds.

I was interested to read this, because I too use =C2=A0that weakened fo= rm
of fibration in some work attempting to get a model of univalence
based only on composition of paths rather than more general Kan
filling operations =E2=80=94 so far unpublished, because I can't qu= ite see how
to get univalent universes to work (but seem frustratingly close to
it).


Very interesting that you also conside= red this form of weakened fibrations! I also thought a bit about basing thi= ngs on a binary composition operation, but I never could get it to work. I = managed to convince myself some year ago that in the presence of connection= s and reversals (potentially with Boolean structure) homogeneous compositio= n (hcomp^0->1) is equivalent to binary composition, but without this str= ucture on the interval I don't really see what to do. But on the other = hand, if you don't have connections then I don't think you need the= fibrations to lift against arbitrary subtubes but rather only open boxes i= n the sense of BCH...

Anyway, the univalent un= iverses (in particular fibrancy of Glue types) is by far the hardest thing = in our note (as seems to always be the case). The way we do it is an adapta= tion of what we did back in CCHM, but because of the weakness we have to do= additional corrections in the construction which makes it quite a bit long= er.
=C2=A0

Anyway, what I wanted to say is that perhaps one should call= these
things "Dold fibrations" by analogy with the classic notion o= f Dold
fibration in topological spaces
<https:/= /ncatlab.org/nlab/show/Dold+fibration>?

Andy

Thanks for the pointer! I didn't k= now about them and will have to think a bit whether what we have could be s= een as a cubical variation of them.

--
<= div>Anders
=C2=A0

--
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_390_1830799272.1550245083753-- ------=_Part_389_1458641519.1550245083753--