From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDTLDGMZRMJBB3H367OAKGQENVVWPWY@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,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.1 Received: from mail-ot1-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b896526a for ; Sun, 16 Sep 2018 06:53:34 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id u40-v6sf7979318otc.0 for ; Sat, 15 Sep 2018 23:53:33 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=J3Rmbi2sTl1Bax2xqssE5Br50Z75X3DqS4JBpNYZ4Bw=; b=A8oyK92z+52K7w8f1TzrUj7R40PEEutMAqzdtqY+5g9gRyt+QHz+QXQVFNo7o4lazq j1a/yOtWbWCrJHWaJfuepbWCUSd1n9y5LKgWbncp2izLfdGkkgP3Vr8tWAEnoc3sunfM XztDqfWJnV2L58J4ZI0/ZpfDBtkfJXWeqnw1XWGwgI0+qx9/3WQHPAkydffXi/mvzADE V0QYmDTbG3wUkDDLloHfTcfy6GrOgpW2FmV2OdhbdG7p7VFoqGBhAmEiklwNUWajZM4l 3YjxKSi5t4m+HjV2sUbKWMggUC/xmB+29WLv+dTT8IOnW/PmE5IGmW2LrtwerT64+FhR uvYA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=J3Rmbi2sTl1Bax2xqssE5Br50Z75X3DqS4JBpNYZ4Bw=; b=hYJNr1cKZ8KiMHFipUEDEs4sDQMgcGQt2fRx9eDkUdMyteZo4Q7aAriW+s94RfbrUI mz7mY5PSySZiCQoHxpsawHPEy7qFgKceQR6LNQkwIUsx9xZXGKpkJB2Z+aHRLnzAUBad zVOpNsnlbB3WalefJ2V4e8PPK6vno7xklXm2s0h+znCf8Vh30T6ue2PDQSYXhMgKLSCG dJMJOKiO7xO8bF/YhPJpAXfljLeIpUdJ3npdCrn/mKa4R+6XUvEpChHfyDmir36gxvbA 9fl0La1SJDqo+rbr6gZV+++YE0dSFnXd1VRm7qwQdGCSrDQsXcAZBdzYLISLV3e0d2sa nRiA== 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: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=J3Rmbi2sTl1Bax2xqssE5Br50Z75X3DqS4JBpNYZ4Bw=; b=sBQzwwxbLfHVpDq0/GhXJUeG52oJV3D8hc7HRobG7ew8S0JqLv3YJWOGvRhpG3gqSP sEkSLJqLgLLxgeiY7BxASxWNlkEyfAG/wIOE+feppl8mGrv+hIWh+Fq3YWFTwTLGe7o6 VoCiQbV4y2B8+ZLGz4EJWZOTADZaFZf9yL1ggy/Xmymk+EbEO8c2F4I705yk9Ukj9BVU yq84Tho9G6xQEPSuu7LBps+n4c7yom6gmDXUOw2XA50sFN5HbGbWOsjOYHt5INACIMo5 peyv5OVsvJVQUAilFvdxmwnNJyhMyr8P48K4tz0pC+hMLekh7h4drkb+mFbZOHYu61nU 0lbA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51DiDFpkTD9MV0SCeQqaFWvVWzjQE5PQ1BvnWVZhdNof60QvKcS3 2GoejaDh1DQ8u8fEBRPvKDs= X-Google-Smtp-Source: ANB0VdZyWAu2kLLVph3eqcJOPYsQmBSwb/dNYCMiS13i7lfii2GQXd0bQ/mJ0MwhBMwwoUrRouumXA== X-Received: by 2002:aca:af15:: with SMTP id y21-v6mr78816oie.6.1537080812164; Sat, 15 Sep 2018 23:53:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:a9d0:: with SMTP id s199-v6ls8508682oie.5.gmail; Sat, 15 Sep 2018 23:53:31 -0700 (PDT) X-Received: by 2002:aca:ec87:: with SMTP id k129-v6mr81296oih.2.1537080811744; Sat, 15 Sep 2018 23:53:31 -0700 (PDT) Date: Sat, 15 Sep 2018 23:53:31 -0700 (PDT) From: Corlin Fardal To: Homotopy Type Theory Message-Id: Subject: [HoTT] 1D W Type? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1369_1398264639.1537080811254" X-Original-Sender: fardalcorlin@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_1369_1398264639.1537080811254 Content-Type: multipart/alternative; boundary="----=_Part_1370_2062947111.1537080811255" ------=_Part_1370_2062947111.1537080811255 Content-Type: text/plain; charset="UTF-8" I've been playing around with a potential general 1D W Type, but I've run across one problem. To give some quick exposition first though, I thought about what it would look like to W-ize the 1D Mu Type posted here a few weeks ago, and realized relatively quickly that it would look more-or-less like the following: data W (F G : Cont) (f g : {X} -> (ContInter F X -> Set) -> Morph G Id) where c : (x : ContInter F (W F G f g)) -> W F G f g e : (x : ContInter G (W F G f g)) -> MorphInter (f c) x = MorphInter (g c) x with some predefined notion of Cont, Morph, and the related terms. Now, Cont should obviously be the standard container found in the standard W type, and Morph seems at first blush like it should be a container morphism, and that almost works. Almost every term the Mu type uses can be pretty straightforwardly defined as a container morphism, but for one: con, the representation of c itself. Now in some ways this seems somewhat obvious, the notion of container morphism is pretty general, and isn't designed including the constructor c, as the syntactic notion of terms are in the Mu type. However, it feels like it should be possible to modify the notion of morphism to suit the needs of representing c, though how exactly that would be done seems somewhat non-obvious to me. So, I guess my question is, can anyone come up with some natural extension of the morphism that accounts for c, or perhaps I'm coming at this from the wrong angle, and there's some other obvious route that I'm missing. -- 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. ------=_Part_1370_2062947111.1537080811255 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I've been playing around with a potential general 1D W= Type, but I've run across one problem. To give some quick exposition f= irst though, I thought about what it would look like to W-ize the 1D Mu Typ= e posted here a few weeks ago, and realized relatively quickly that it woul= d look more-or-less like the following:
data W (F G : Cont) (f g : {X} = -> (ContInter F X -> Set) -> Morph G Id) where
=C2=A0c := (x : ContInter F (W F G f g)) -> W F G f g
=C2=A0e : (x : Con= tInter G (W F G f g)) -> MorphInter (f c) x =3D MorphInter (g c) x
=
with some predefined notion of Cont, Morph, and the related terms. Now= , Cont should obviously be the standard container found in the standard W t= ype, and Morph seems at first blush like it should be a container morphism,= and that almost works. Almost every term the Mu type uses can be pretty st= raightforwardly defined as a container morphism, but for one: con, the repr= esentation of c itself. Now in some ways this seems somewhat obvious, the n= otion of container morphism is pretty general, and isn't designed inclu= ding the constructor c, as the syntactic notion of terms are in the Mu type= . However, it feels like it should be possible to modify the notion of morp= hism to suit the needs of representing c, though how exactly that would be = done seems somewhat non-obvious to me. So, I guess my question is, can anyo= ne come up with some natural extension of the morphism that accounts for c,= or perhaps I'm coming at this from the wrong angle, and there's so= me other obvious route that I'm missing.

--
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_1370_2062947111.1537080811255-- ------=_Part_1369_1398264639.1537080811254--