From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBPUBUDMQKGQESF4BHDI@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.6 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-ot0-x239.google.com (mail-ot0-x239.google.com [IPv6:2607:f8b0:4003:c0f::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ede50ac1 for ; Mon, 18 Jun 2018 18:58:07 +0000 (UTC) Received: by mail-ot0-x239.google.com with SMTP id a25-v6sf10606903otf.2 for ; Mon, 18 Jun 2018 11:58:07 -0700 (PDT) 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=DmyfS/610eLkHS7NDdIwEtqGoJHPn/zOb72ZnmMJoro=; b=MgKyEWi83nF63gDxBXclfXKLlSj5EtebL0r1tsw/1ARcvCAp5dyqJ1B6V+Rx9m6Z4l H+T6RkqWITo1uvf7zr80OobAClhWaEMbc0PNrVZFx6lrHR/HQgaFQYuyFDHynVv4RUiq 4kB+FucSwT9uwBTvkMEKLl/fdaaEjK5Y4oeDRq73yvW5LUayMlnfJlo/16k2nvCcjHPP wTVR/F2q+28PQryA7g2bNLcVQmm7a+QZBoQZ4NoJS1kDa2O6chkUVbDiU+lB3Lj0R/el qrOwn7qGX9+SiMjFz3KDGJ/qmacvzQz6H2TF/Fa16Cw/4KON5NVvNBr5IV0EicbRAumJ 8OXA== 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=DmyfS/610eLkHS7NDdIwEtqGoJHPn/zOb72ZnmMJoro=; b=YvwJvd7fZr1fTPLmaq7/xPGt2ql38vY9Q1Cf6uIM/DrcFiWFs41eAp9zKAlE1NWXTB Vy2cAGsm3AL4uOJttlF3a/I9zvHhZpjVB/CiALuNA0ml0OVPBs9BTYLhbH71IhCvm4wE xuzBtEWNx9Axh9z7WjHX5h/yBPgJ+FYw8CBkb1doK1IYOeiGhPDkoA4TAjVC1RLHvl/7 8W0ZY6F4fNo129cEfprViDnzQwOtatBWcd1c7JEFrUNEs+NtE1+xs/FNjtpxBkb8MXUB wXxmE/DHp8T2jOEyJ84RNASdEAecB5buNaN1HedCBNs766jk6zxQDYGkDN7GM/fA1Nfd 9K3g== 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=DmyfS/610eLkHS7NDdIwEtqGoJHPn/zOb72ZnmMJoro=; b=aWpAy6Shu3/ZpFJULAntj0MKAPIQgiqmXn0MAb0ogVymZt/1+vu7o8NwZ02nQsPG3R pJJtXzWaBqE8ztTBYF11cKE3hixFAt+r8dJgdtJ6+QB/BY3mNUd9H7UR4b+lK+oWds5O FjWPkYGSrVYJ2hOsfva0cZNYVYnOpRPkyMnMn5/xqe3gxyPzPFY5cWGqP/DK2VhymK3d 6RfAT62jXP/Weeh43If+Gp9tgD9cXMVjfdhrU3tHIsizuwg3X3Ib+jK1iHy8hBWW/i33 +xwrOiW1oL4kDM3zdc8PaNMFfumgpZFfVpxNOTLlKeX8qoC9m5vxyE3jUeoPr174xNoK lqMw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E2FJwtMjesvRZ5doP9fMwASqqIbfeahNS+3lqlAZd9tdElb/JDc B/be7OEcfPg+hIEvvWEH2H4= X-Google-Smtp-Source: ADUXVKInnJ6OZ6xbffDT9A1E8gTVUqfFmKNl7Cvf5XblHSYC3MoBR06TnkNeNQJ6K6WKarv8mSzfew== X-Received: by 2002:a9d:190a:: with SMTP id j10-v6mr567552ota.0.1529348286622; Mon, 18 Jun 2018 11:58:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4c99:: with SMTP id m25-v6ls6600999otf.0.gmail; Mon, 18 Jun 2018 11:58:06 -0700 (PDT) X-Received: by 2002:a9d:4c96:: with SMTP id m22-v6mr579571otf.6.1529348286232; Mon, 18 Jun 2018 11:58:06 -0700 (PDT) Date: Mon, 18 Jun 2018 11:58:05 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_11064_1157457530.1529348285692" X-Original-Sender: atmacen@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_11064_1157457530.1529348285692 Content-Type: multipart/alternative; boundary="----=_Part_11065_558411489.1529348285692" ------=_Part_11065_558411489.1529348285692 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, Xieyuheng. On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote: > > is there a categorical construction to generalize arrow composition, > by allowing domain and codomain to be refined (or changed) by the > composition ? > > this construction would be useful for > forming theoretical background of dependent type system. > > for example, compose two functions > f : (A x -> B y) > g : (B n -> C z) > will give us a function of type (A n -> C z) > I can't figure out what rule you're using to get that type. If n unifies=20 with y, how did x become n also? That's what I'm guessing you're trying. > another example would be the following generalized composition in=20 > cartesian closed category : > f : (t1, t2) -> (t3, t4) > g : (t, t3, t4) -> (t6, t7) > f;g : (t, t1, t2) -> (t6, t7) > and > f : (t1, t2) -> (t, t3, t4) > g : (t3, t4) -> (t6, t7) > f;g : (t, t1, t2) -> (t, t6, t7) > this can be called `cut` > because it looks like gentzen's cut rule in sequent calculus, > and it can be used to provide semantic > for a stack based concatenative programming language. > This looks more like a combination of composition and tensoring, in a=20 monoidal category. Based on some stuff in a blog post=20 (https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivari= a.html),=20 the cut rule is instead composition in a polycategory, and you can only cut= =20 out one type at a time. I'm thinking the first "generalized composition" could be explained thus: f only looks at the top two stack elements, and replaces them with three=20 others. But the stack generally has additional elements, which I'll=20 abstract away as =CE=93: f : (=CE=93, t1, t2) -> (=CE=93, t3, t4) g has a similar story, but we use a different stack/context variable to=20 avoid accidental constraints: g : (=CE=94, t, t3, t4) -> (=CE=94, t6, t7) To compose these, we need (=CE=93, t3, t4) to unify with (=CE=94, t, t3, t4= ), so (=CE=93=20 :=3D =CE=94, t), and f;g : (=CE=94, t, t1, t2) -> (=CE=94, t6, t7) which we shorten to (t, t1, t2) -> (t6, t7). So your composable operators seem to be substitutions (morphisms between=20 contexts) that are polymorphic in most of the context. All but a finite=20 chunk all the way on the right. Composition would presumably be composition= =20 of substitutions, after instantiating them with the principal unifier. For simply-typed systems, contexts and substitutions can be modeled in a=20 monoidal category, which includes cartesian closed categories. For=20 dependent type systems, other kinds of categories are used, like contextual= =20 categories and categories with families; hopefully what you want is still= =20 instantiation and composition of this new kind of substitution. I'm not an expert on the kinds of categorical structures involved, but=20 hopefully polymorphic substitutions is a good way of thinking about what=20 you're doing, which connects it with categorical models. Beware that with dependent types, there generally are not principal=20 unifiers, due to binding operators appearing in types. But concatenative=20 people don't seem to like binders, so maybe you dodged the bullet. --=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_11065_558411489.1529348285692 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi, Xieyuheng.

On Monday, June 18, 2018 at 12:32:14= PM UTC-4, xieyuheng wrote:
is there a categorical construction to generalize arrow compo= sition,
by allowing domain and codomain to be refined (or changed) by th= e
composition ?

this construction would be useful for
forming = theoretical background of dependent type system.

for example, compos= e two functions
f : (A x -> B y)
g : (B n -> C z)
will give = us a function of type (A n -> C z)

I can&= #39;t figure out what rule you're using to get that type. If n unifies = with y, how did x become n also? That's what I'm guessing you'r= e trying.


another example would be the following generalized compositio= n in cartesian closed category :
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 f=C2=A0=C2=A0 : (t1, t2) -> (t3, t4)
=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0 g=C2=A0=C2=A0 : (t, t3, t4) -> (t6, t7)
=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f;g : (t, t1, t2) -> (t6, t7)
and
= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f=C2=A0=C2=A0 : (t1, t2) -> (= t, t3, t4)
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 g=C2=A0=C2=A0 : (t= 3, t4) -> (t6, t7)
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f;g : (= t, t1, t2) -> (t, t6, t7)
this can be called `cut`
because it look= s like gentzen's cut rule in sequent calculus,
and it can be used to= provide semantic
for a stack based concatenative programming language.<= br>

This looks more like a combination of compos= ition and tensoring, in a monoidal category. Based on some stuff in a blog = post (https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_mult= ivaria.html), the cut rule is instead composition in a polycategory, and yo= u can only cut out one type at a time.

I'm thinking the first &q= uot;generalized composition" could be explained thus:
f only looks = at the top two stack elements, and replaces them with three others. But the= stack generally has additional elements, which I'll abstract away as = =CE=93:
f=C2=A0 :=C2=A0 (=CE=93, t1, t2) -> (=CE=93, t3, t4)

g= has a similar story, but we use a different stack/context variable to avoi= d accidental constraints:
g=C2=A0 :=C2=A0 (=CE=94, t, t3, t4) -> (=CE= =94, t6, t7)

To compose these, we need (=CE=93, t3, t4) to unify wit= h (=CE=94, t, t3, t4), so (=CE=93 :=3D =CE=94, t), and
f;g=C2=A0 :=C2=A0= (=CE=94, t, t1, t2) -> (=CE=94, t6, t7)
which we shorten to (t, t1, = t2) -> (t6, t7).

So your composable operators seem to be substitu= tions (morphisms between contexts) that are polymorphic in most of the cont= ext. All but a finite chunk all the way on the right. Composition would pre= sumably be composition of substitutions, after instantiating them with the = principal unifier.

For simply-typed systems, contexts and substituti= ons can be modeled in a monoidal category, which includes cartesian closed = categories. For dependent type systems, other kinds of categories are used,= like contextual categories and categories with families; hopefully what yo= u want is still instantiation and composition of this new kind of substitut= ion.

I'm not an expert on the kinds of categorical structures in= volved, but hopefully polymorphic substitutions is a good way of thinking a= bout what you're doing, which connects it with categorical models.
<= br>Beware that with dependent types, there generally are not principal unif= iers, due to binding operators appearing in types. But concatenative people= don't seem to like binders, so maybe you dodged the bullet.
<= /div>

--
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_11065_558411489.1529348285692-- ------=_Part_11064_1157457530.1529348285692--