From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGPPLV76EPRBPU3ULMQKGQE3CKEERA@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-x23c.google.com (mail-ot0-x23c.google.com [IPv6:2607:f8b0:4003:c0f::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a412e721 for ; Tue, 19 Jun 2018 04:59:44 +0000 (UTC) Received: by mail-ot0-x23c.google.com with SMTP id a1-v6sf11026515oti.8 for ; Mon, 18 Jun 2018 21:59:43 -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=e09bjuZBcOISRlZHFTnmu0DC2IHHqv0GiQQQtMfIlRg=; b=QA4unYOkFJ/5RbxbTg9ttpuJUroCUNxYIb2PI3mGrHIthmCJcV8X4a3BvLyJHR9cJH KZne7U1oDrf90SUMCCqTYFbqjhwpId1VjHYbMD3DKMfjRWVswUevcY37RiTVa5JxEMi4 vfbwBmtEGadEm8C9WotfDhLxi7vnprkIoiDoHorCZ+Actg/LCsKoxHFS9P/O3rZ1UuDK lxtEkiooO9thhEuyoMFgrPVQnD5ww/cfGq3JdkPt6ldb9u4r1oGJY4Cak7L+5IbQZJwP U8057oSZJSKW6dxgXKeqMgv3L/hF2WYzOv63D/oboI4cAywxjmjkb4Ko6gKdFGrp5iGJ rtbA== 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=e09bjuZBcOISRlZHFTnmu0DC2IHHqv0GiQQQtMfIlRg=; b=jco9HWhcIwfUq/gCeAAHyLWZhxPAiTHye7QQQ41y5QCkroheaPKrU9TRt5A8Q4G9t9 9ZdJbgX0CK60h88/sdxwxpyVcRmbp7QnXe//jRSfI65SZg2DtKme7W702cJfBBcFhN8D n77uPKp0Iz9GnouhERa5ogGpIb7oXPfreeZvZ9e01w7X0pCoSAzB8V4rajfXkfvJi5FW 2NcnkVWNb2nKaGfJIiPpLQsxwEWw3k8jQ8Jl/FXeIjqrhtvfcYuD2zP6ssoj7npNQj04 JU81IAv//7RSj+JvQuNaHvKcYEdbVVq2IRwuFdbxwbMwyoy4nGWiC4ZARfMgZA8aOa2Q dlAQ== 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=e09bjuZBcOISRlZHFTnmu0DC2IHHqv0GiQQQtMfIlRg=; b=MuBwUi8PPF3AaFUcTeYiK6y85EAKdQI9q4zgCYB7Cs+dVhi6prq6OLzp1w3mLWfJRb j7vCnRZ/yLYq3tDMBggPRMdVQA9sjQ/DtHQaB0R5lbQATmeyonoUOERn6tzM4486+Njp 1zh3G7QtLkpZEbh30TuAHi41s0PEljBlfbBFeJGmG1DQ5qkZEP/YEKpgjgIxJRkkhy+E hajWsE6XvhPJHJBDUtcORQBt0pwyznwlg3Z1Tx7ROOF1bAfpRREqa6KL4u0aB5WLMxJG uBHJLsOjjdkuTCgY0Pq9R+h+4teAFxU3bp6x5r+4grpQ3wpjOmc+SJlj69D4GsossPXm /PIg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E1eyy75heLubqNzQvKoFFm7P9tQixkMQdXpqr3w9+vv/FAOnlhf xpcWyH5yldqeC6j1X6fnBp4= X-Google-Smtp-Source: ADUXVKImvJEm+Tk+x6RzdTlssd2FfLnoY4OfPcV6zRXnwuKzuPFVL36LnKCYSMgpCKkJayY3Ax+SoA== X-Received: by 2002:aca:abc6:: with SMTP id u189-v6mr652617oie.2.1529384382514; Mon, 18 Jun 2018 21:59:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:63d1:: with SMTP id e17-v6ls7083776otl.14.gmail; Mon, 18 Jun 2018 21:59:42 -0700 (PDT) X-Received: by 2002:a9d:70c2:: with SMTP id w2-v6mr635949otj.2.1529384382037; Mon, 18 Jun 2018 21:59:42 -0700 (PDT) Date: Mon, 18 Jun 2018 21:59:41 -0700 (PDT) From: xieyuheng To: Homotopy Type Theory Message-Id: In-Reply-To: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> References: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> 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_18174_878913687.1529384381564" X-Original-Sender: xyheme@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_18174_878913687.1529384381564 Content-Type: multipart/alternative; boundary="----=_Part_18175_1099759687.1529384381565" ------=_Part_18175_1099759687.1529384381565 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable sorry, I had a typo, the first example should be : f : (A x -> B x) g : (B n -> C z) will give us a function of type (A n -> C z) On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Oliveri wrote: > > 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 ( > https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivar= ia.html),=20 > the cut rule is instead composition in a polycategory, and you can only c= ut=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 compositi= on=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 contextu= al=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_18175_1099759687.1529384381565 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
sorry, I had a typo, the first example should be :
=C2= =A0=C2=A0=C2=A0 f : (A x -> B x)
=C2=A0=C2=A0=C2=A0 g : (B n -> C = z)
=C2=A0=C2=A0=C2=A0 will give us a function of type (A n -> C z)

On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Oliveri wrote:=
Hi, Xieyuheng= .

On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote:
is there a categorica= l construction to generalize arrow composition,
by allowing domain and c= odomain to be refined (or changed) by the
composition ?

this cons= truction 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 with y, how did x become n also? Th= at's what I'm guessing you're trying.


another example would be t= he following generalized composition 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 : (t3, 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 looks like gentzen's cut rule in sequent= calculus,
and it can be used to provide semantic
for a stack based c= oncatenative programming language.

This look= s more like a combination of composition and tensoring, in a monoidal categ= ory. Based on some stuff in a blog post (https://golem.ph= .utexas.edu/category/2017/11/the_polycategory_of_multivaria.= html), the cut rule is instead composition in a polycategory, and you c= an only cut 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 others. But the st= ack 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 ha= s a similar story, but we use a different stack/context variable to avoid a= ccidental 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 with (= =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 substituti= ons (morphisms between contexts) that are polymorphic in most of the contex= t. All but a finite chunk all the way on the right. Composition would presu= mably be composition of substitutions, after instantiating them with the pr= incipal unifier.

For simply-typed systems, contexts and substitution= s can be modeled in a monoidal category, which includes cartesian closed ca= tegories. For dependent type systems, other kinds of categories are used, l= ike contextual categories and categories with families; hopefully what you = want is still instantiation and composition of this new kind of substitutio= n.

I'm not an expert on the kinds of categorical structures invo= lved, but hopefully polymorphic substitutions is a good way of thinking abo= ut what you're doing, which connects it with categorical models.
Beware that with dependent types, there generally are not principal unifie= rs, due to binding operators appearing in types. But concatenative people d= on't seem to like binders, so maybe you dodged the bullet.

--
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_18175_1099759687.1529384381565-- ------=_Part_18174_878913687.1529384381564--