From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBGVFUXMQKGQEZI75P5A@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-oi0-x238.google.com (mail-oi0-x238.google.com [IPv6:2607:f8b0:4003:c06::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c9035be5 for ; Tue, 19 Jun 2018 18:59:41 +0000 (UTC) Received: by mail-oi0-x238.google.com with SMTP id e10-v6sf360579oig.16 for ; Tue, 19 Jun 2018 11:59:40 -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=2mGI4NzNbLZHp0SBY440XvwYiIOtPa5how6Y/FRtbQ4=; b=DKqyRK6O8PiyrRTMDUiQfpJl1xM3gFUCrhqbjvtwWG5owRq3ZQkoKmRhc5khr6qREH aZ+7ZG6vCPD5QtGO28WIArcEPYsNju9BBFhKhknHCLM884gCtKNb9A4gwoFol8re+Ii9 CRKzmvYJ+qE4rX62RyTd30rYJRzffjboOXNuktJjVex6DpTSZDyu8pCS4iWmRinndoQI GrfQzqcm028JPNKT0QmspmOunoCeomRGvNahiUHIJc7/UnsTGFAkqF+zOdPIUCYFmsrD PCSbikg/R6XCNwmaBY+l69JBnhwMNdVOmNoBdzMfhmKs68COdB8sS2A8+l3vIvkw49Wo kk2w== 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=2mGI4NzNbLZHp0SBY440XvwYiIOtPa5how6Y/FRtbQ4=; b=oVB8mLUa3+Pkw+cwvICdfT96KW6yjuVBFqvchdOsCr5WN6pf/ZzKW86md+YItUaA9Y C8UgtZQH3WOZ6bvqIkFqitaXa8EQjYzUjSA3RXGPFMN3ks7p9O6cEbzRDq5nN+5te8al gLQFAINYxHBBLwF5z2sTFaSBsHii9dOOoop7Njg3xasnOpF+n88/oPJIuDtD5FASU0D7 gs/xFkrQvIaSwAyUmwFjf5DBwZmq/7xlu2uRUrXXviJ+o+AJ/vyNx/zGrUtPRUT4+JJI IqMXYXvKb/QvrgfDzVLKI0IGZDOk+SQsOrNtGmzALVCBcxdxrQ1NbrsZAbiVthgzZxnM F9pA== 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=2mGI4NzNbLZHp0SBY440XvwYiIOtPa5how6Y/FRtbQ4=; b=cxr1mElFv5vvFzYIx3EvtdbsuLy6+UMQTih2QyQuNg8cpwtpRkPGqRLnXktj5Jz0gf xOYk2DBIlCgb98jEgZ050z8NmaoztJzz1PZtHyDmnpuiWElDezF1sCaJ9QGukEyKmoB6 +TpvPmTjDWocJTu1e8qaQcen2vtsGL6VPoKlPH63zQ4S45Ln71ZNZM2N6XlbNAYbw6jm MSLPlHT0J/9GJUGFO6nZImlknnfayS5/CPN/k2gpfHC9jk3O35bWoQoCuco3bqwvFdAS qu4USYu3fZCr1NacM+5R2kXOJZVi7GVb6S527LZnO5dA80XFrMGlqZU9mhNapkdEm1tj qxWg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E35Ikt8r1nUu4MOOuVnj1IuDApGL/Pgagze5wp7ZQ/G2rF+8os7 ZXm8gA4PN/pBu9XVUSK4+Ms= X-Google-Smtp-Source: ADUXVKJ8jmM1weLGYxvQRks4/s/SM66xOwOuY/Wr0zyfqkFCHjGS9Ee8HKd7TMIl9hxkqpaIXVHoig== X-Received: by 2002:aca:1a18:: with SMTP id a24-v6mr741809oia.5.1529434779078; Tue, 19 Jun 2018 11:59:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:4dcc:: with SMTP id a195-v6ls160903oib.13.gmail; Tue, 19 Jun 2018 11:59:38 -0700 (PDT) X-Received: by 2002:aca:d60f:: with SMTP id n15-v6mr758588oig.6.1529434778741; Tue, 19 Jun 2018 11:59:38 -0700 (PDT) Date: Tue, 19 Jun 2018 11:59:38 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <9b68a44e-7c9c-451b-8aab-a7a4c972ba6c@googlegroups.com> In-Reply-To: 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_13903_1845284932.1529434778278" 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_13903_1845284932.1529434778278 Content-Type: multipart/alternative; boundary="----=_Part_13904_451191729.1529434778278" ------=_Part_13904_451191729.1529434778278 Content-Type: text/plain; charset="UTF-8" On Tuesday, June 19, 2018 at 4:07:34 AM UTC-4, xieyuheng wrote: > > I will learn more about polycategory and polymorphic, > and try to use them to explain dependent type system. > > thank you again :) > So polycategories had to do with the cut rule, which is not what your examples are doing. I don't think you need to worry about polycategories. I don't think there's much connection between polycategories and polymorphism, other than the prefix "poly". The kind of polymorphism I used on your example is "row polymorphism". This was already used for typing the "Cat" concatenative language. (So I was guessing you already knew about it, otherwise I would've said so earlier.) Thinking of the underlying monomorphic (non-polymorphic) stack types as contexts, I figure the approach should generalize to dependent contexts, with the operations being polymorphic substitutions between dependent contexts. So I think the ingredients you want are some dependent generalization of row polymorphism, and some categorical approach to interpreting the underlying monomorphic contexts and substitutions, like contextual categories. There are a lot of approaches to categorical interpretations of dependent types, and I don't know very much about it. This overview page knows more than I do: https://ncatlab.org/nlab/show/categorical+model+of+dependent+types -- 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_13904_451191729.1529434778278 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Tuesday, June 19, 2018 at 4:07:34 AM UTC-4, xieyuheng w= rote:
I will l= earn more about polycategory and polymorphic,
and try to use them to exp= lain dependent type system.

thank you again :)

So polycategories had to do with the cut rule, which is not what = your examples are doing. I don't think you need to worry about polycate= gories. I don't think there's much connection between polycategorie= s and polymorphism, other than the prefix "poly".

The kind= of polymorphism I used on your example is "row polymorphism". Th= is was already used for typing the "Cat" concatenative language. = (So I was guessing you already knew about it, otherwise I would've said= so earlier.) Thinking of the underlying monomorphic (non-polymorphic) stac= k types as contexts, I figure the approach should generalize to dependent c= ontexts, with the operations being polymorphic substitutions between depend= ent contexts.

So I think the ingredients you want are some dependent= generalization of row polymorphism, and some categorical approach to inter= preting the underlying monomorphic contexts and substitutions, like context= ual categories.

There are a lot of approaches to categorical interpr= etations of dependent types, and I don't know very much about it. This = overview page knows more than I do:
https://ncatlab.org/nlab/show/catego= rical+model+of+dependent+types

--
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_13904_451191729.1529434778278-- ------=_Part_13903_1845284932.1529434778278--