From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGPPLV76EPRBRXTULMQKGQEH7DH3BY@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-x23a.google.com (mail-ot0-x23a.google.com [IPv6:2607:f8b0:4003:c0f::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a8480c12 for ; Tue, 19 Jun 2018 08:07:36 +0000 (UTC) Received: by mail-ot0-x23a.google.com with SMTP id v37-v6sf11466440ote.10 for ; Tue, 19 Jun 2018 01:07:36 -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=T14nw7YAvqV+r7QDmM0vNDz8DsXhAxyzvMGAAYsP7fo=; b=gj6Q1PDjQccK96akrMsN9vwQNS3MXW/Rm9zFxSZWV4oE3BFMtYBkLNOuvoB8UPFipR NholwTQOH1S9mWVGurzbgxwNVMaCzN+mo5EIdvb/rCFOYb1L48NiACJnQNehyQ2dO+eP 7WiKLfzjQtxmsTMWnujyGESgzaFdbhI52H+4Yh1yXWzrVbStHov5Wci5TqBsYJHqCLTb 4anbtrRUv69bUGrc161TBtyq8A9rkhEjo/LLdIvEJCxJkt4zbE5gpM/LtkY0CDeRDppd KympG2GET8vw/TGhbCSiaDSVCdMJBfYheW+LCmF3NgvbWbyCWYXKIGicdV0tm3jv1s0S uong== 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=T14nw7YAvqV+r7QDmM0vNDz8DsXhAxyzvMGAAYsP7fo=; b=MM+Ij3YrngQVA4Q4CfDsVZJ43KBl+GlYRpPpuAMVyh5vVl5bIkYKOthT+n0yMRqdvb ular+zZ5vkj5hQQ80qpzx/TqtVOCplWlZjuBySkMIaMdh+8HRcnefHB61DCzIdCQ/hIq jR0Y9h8WsIkjMMQ/b+6VQy+tXoOFdFt1TfldmoAWReDB9cqEd8EgPlLkmxh+SPBO0cmd BunroR1XB2Wwg/JNqjekZPiKioy1nfCR4rJa6CCm/S1u/mjPAYeAjf8mVF+dNmOQVZQ3 7zv4YVApzDc4L2yvB9/KhaIJqfNeraDXXeA5L/z62A3FZgycQzZIR+Dy+UlBpGnvZ9cP ld8A== 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=T14nw7YAvqV+r7QDmM0vNDz8DsXhAxyzvMGAAYsP7fo=; b=mEiAoX8aF49nA+mrSvRaAXr6DTan2zrw5BeWUKjoDULAhYnj4lAcuXQWaA/6CRHveT 3gb4qgjdqzkaWpC/jPKU68wcPatjXQEHLfHpMg0u9ImjoFJxls1YgnFuMRv7IFt4JBas Zc8BFGDQdFK/85214RE/HnLrgat41Z9MdgFoU9Vr0y5o/QxkMNGkSyXCc1c6Wc+pghVq fSgmB97sIZ016L/W/ueI+DAPMK5bf9qWnu2LER+kR9enzBTOgURGE5FQtclkqpU5WGiE BwpR3YqTSalEsDLtTmvHsGlmBjKbVlIHXd50jnY1pFYK48joBsKUNvPw6ASNrC61dJTa /avQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E0T2xB3uKiDZvx7YVwWcBazKIgERgCvXqjYwOPAtTT37JM2BiYr CADAIjZmDaEuG/rt11oo+X0= X-Google-Smtp-Source: ADUXVKIQztMo67hHs686PdMCG/qnFjsu4SsiKSkSeTJHXF9MA79UJpR9dNh8KsZk3ykeG1rtpQfgbA== X-Received: by 2002:aca:d60f:: with SMTP id n15-v6mr662446oig.6.1529395654869; Tue, 19 Jun 2018 01:07:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5c85:: with SMTP id a5-v6ls6603409oti.16.gmail; Tue, 19 Jun 2018 01:07:34 -0700 (PDT) X-Received: by 2002:a9d:4b04:: with SMTP id q4-v6mr675100otf.3.1529395654525; Tue, 19 Jun 2018 01:07:34 -0700 (PDT) Date: Tue, 19 Jun 2018 01:07:33 -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_18603_1980633507.1529395654084" 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_18603_1980633507.1529395654084 Content-Type: multipart/alternative; boundary="----=_Part_18604_1953867952.1529395654084" ------=_Part_18604_1953867952.1529395654084 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable thank you Matt Oliveri. the substitutions you used above explains my examples perfectly. I also found a bug in my second examples : f : (A, t1, t2) -> (A, t, t3, t4) g : (B, t3, t4) -> (B, t6, t7) (unify) B =3D (A, t) f : (A, t1, t2) -> (A, t, t3, t4) g : (A, t, t3, t4) -> (A, t, t6, t7) f;g : (A, t1, t2) -> (A, t, t6, t7) (shorten) f;g : (t1, t2) -> (t, t6, t7) (but I mistakenly wrote) f;g : (t, t1, t2) -> (t, t6, t7) --- I will learn more about polycategory and polymorphic, and try to use them to explain dependent type system. thank you again :) ------ xieyuheng 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_18604_1953867952.1529395654084 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
thank you Matt Oliveri.

the substitutions you used = above explains my examples perfectly.
I also found a bug in my second ex= amples :

f=C2=A0=C2=A0 : (A, t1, t2) -> (A, t, t3, t4)
g=C2=A0= =C2=A0 : (B, t3, t4) -> (B, t6, t7)

(unify)
B =3D (A, t)
f=C2=A0=C2=A0 : (A, t1, t2) -> (A, t, t3, t4)
g=C2=A0=C2=A0 : (A, t= , t3, t4) -> (A, t, t6, t7)

f;g : (A, t1, t2) -> (A, t, t6, t7= )

(shorten)
f;g : (t1, t2) -> (t, t6, t7)

(but I mistak= enly wrote)
f;g : (t, t1, t2) -> (t, t6, t7)

---

I will= learn more about polycategory and polymorphic,
and try to use them to e= xplain dependent type system.

thank you again :)

------
xieyuheng


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, xieyu= heng wrote:
is ther= e a categorical construction to generalize arrow composition,
by allowin= g domain and codomain to be refined (or changed) by the
composition ?
this construction would be useful for
forming theoretical backgroun= d 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 bec= ome n also? That's what I'm guessing you're trying.


another exam= ple would be the following generalized composition in cartesian closed cate= gory :
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f=C2=A0=C2=A0 : (t1, t= 2) -> (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 concatenative programming language.

This looks more like a combination of composition and tensoring, in a= monoidal category. Based on some stuff in a blog post (h= ttps://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_m= ultivaria.html), the cut rule is instead composition in a polycate= gory, and you can 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 oth= ers. But the stack generally has additional elements, which I'll abstra= ct away as =CE=93:
f=C2=A0 :=C2=A0 (=CE=93, t1, t2) -> (=CE=93, t3, t= 4)

g has a similar story, but we use a different stack/context varia= ble to avoid 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) t= o 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 substitutions (morphisms between contexts) that are polymorphic in most = of the context. All but a finite chunk all the way on the right. Compositio= n would presumably be composition of substitutions, after instantiating the= m with the principal unifier.

For simply-typed systems, contexts and= substitutions can be modeled in a monoidal category, which includes cartes= ian closed categories. For dependent type systems, other kinds of categorie= s are used, like contextual categories and categories with families; hopefu= lly what you want is still instantiation and composition of this new kind o= f substitution.

I'm not an expert on the kinds of categorical st= ructures involved, but hopefully polymorphic substitutions is a good way of= thinking about what you're doing, which connects it with categorical m= odels.

Beware that with dependent types, there generally are not pri= ncipal unifiers, due to binding operators appearing in types. But concatena= tive people don'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_18604_1953867952.1529395654084-- ------=_Part_18603_1980633507.1529395654084--