From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGPPLV76EPRBD55T7MQKGQEL6PTYFY@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-x23b.google.com (mail-ot0-x23b.google.com [IPv6:2607:f8b0:4003:c0f::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0f595149 for ; Mon, 18 Jun 2018 16:32:17 +0000 (UTC) Received: by mail-ot0-x23b.google.com with SMTP id p12-v6sf10373376oti.6 for ; Mon, 18 Jun 2018 09:32:17 -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=wxGY9dLCVhCSgImM0vDUNSJn9MW92Yw68C34gNX5CHs=; b=piaBNpUZF3FVqicYzAGemSfA9voBf8f98zyUunzIVSbHs6LNHIoCqbxVaVCzKQuPBR mlLEHp/P+98A+PUxQj+/ulDtwoBXxIranot+hfbx6qZbArhxLbcS8QwhqKTjsmDnnsMu qx4dW6rpvTAhHut+NnMXbkeibl4T3CxT8+PS7SpmcWyazPfH1V/HBlU3XFtSbwNwfgHk 2LVfeZvtLpVuBxf5WnBfAVqi7vV7Y+wxrxEvJmzLekopWHQmTcKwfIZk87BMw+iZj19D 3pbAcsx7Wywdyx5S9x5mwz1XsiP1bpYSsURU05xeRpisv/ydAe5DRSnjDPHuhHBoETBy EJgQ== 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=wxGY9dLCVhCSgImM0vDUNSJn9MW92Yw68C34gNX5CHs=; b=hHEn/NGSAB0Ec9cKzI1y02xn9uT04s/UM0SdrWmkrEBpfHsrFVAy8DdPP8QOoXRMwp YwZFTa9MSLlSDhF+BYJ9RKwoEzd1392jJCZP6df/xwiQo5vKeFIaZNXedrjdHdGhnQVe 7Q/MriTYJNL5G3vtsmo5Y6FYUZNjv9oCWajFQW9S+EVtiNxX1Qc9PuXUzVlCtJ2bpFXv NQXlRXLFzb3jI/fcBGfHLVjh0IDXaKnXYOmak3uw3HUWjE/eGwo+/wybwYau2EyQNIe8 VaJQCT7DsT5uXyxasRNval/GaIAvoShlBGy1tgZmT4fch0SwNaI11Lv6h6lpkvtW270K j/8g== 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=wxGY9dLCVhCSgImM0vDUNSJn9MW92Yw68C34gNX5CHs=; b=TXanvbBRA1IUaSE8EQV71QWE2vEXV94Fct825mabWCoyyjOGkDTIz+VgjmN7mfn9Rg 2EOh/bDFqxI0+8L/h1Oxj9B/d56csZU0TS2DWZdr8TeThpSaiF0KIrjgc7tVQy2CSka6 I/7opy+YyeJXbxWcEKWA92asCFKtbJf672b0UIrMgtPlpP9puLtMmfxe1D2yu7YqbISS 5vKxUCjsiWlsp/0zbx1QEwCN64wStSpK6amcDtuhUrGF35Y135HftCoLf7pL6bFLSq16 W6crLsgiriQc7Qr4rCIjD0F0ujTPu95DXcvB5PtHeGBfMCwbftOCUajnxRAYCJho0BrF XJTw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E2ZThKcPr/9bAtOYp+TK/HGtd9s2mpQNPt5tTTqXNEAPpzH/1rt as8e+PWiEOUQa7VfOQTc+2o= X-Google-Smtp-Source: ADUXVKJP/5Sfkkp9IwD2sG2tUbcV9Lg8F2ABNJNViociscsYSsPH4t669IbdX+xYsBQ60dDfXd/QOQ== X-Received: by 2002:a9d:296a:: with SMTP id d97-v6mr541286otb.1.1529339535513; Mon, 18 Jun 2018 09:32:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:2b13:: with SMTP id i19-v6ls5641120oik.2.gmail; Mon, 18 Jun 2018 09:32:15 -0700 (PDT) X-Received: by 2002:aca:d60f:: with SMTP id n15-v6mr540443oig.6.1529339535005; Mon, 18 Jun 2018 09:32:15 -0700 (PDT) Date: Mon, 18 Jun 2018 09:32:14 -0700 (PDT) From: xieyuheng To: Homotopy Type Theory Message-Id: Subject: [HoTT] 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_16135_961912032.1529339534455" 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_16135_961912032.1529339534455 Content-Type: multipart/alternative; boundary="----=_Part_16136_230797826.1529339534455" ------=_Part_16136_230797826.1529339534455 Content-Type: text/plain; charset="UTF-8" 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) another example would be the following generalized composition in 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. ------ xieyuheng -- 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_16136_230797826.1529339534455 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
is there a categorical construction to generalize arrow co= mposition,
by allowing domain and codomain to be refined (or changed) by= the
composition ?

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

for example, com= pose two functions
f : (A x -> B y)
g : (B n -> C z)
will gi= ve us a function of type (A n -> C z)


another example would b= e the 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, t= 3, 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 sequ= ent calculus,
and it can be used to provide semantic
for a stack base= d concatenative programming language.


------
xieyuheng

--
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_16136_230797826.1529339534455-- ------=_Part_16135_961912032.1529339534455--