From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGPPLV76EPRBDO4U7MQKGQEGMVSQ6I@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-x23c.google.com (mail-oi0-x23c.google.com [IPv6:2607:f8b0:4003:c06::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ef79eb8f for ; Wed, 20 Jun 2018 06:02:54 +0000 (UTC) Received: by mail-oi0-x23c.google.com with SMTP id j136-v6sf1289290oih.13 for ; Tue, 19 Jun 2018 23:02:54 -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=NaZjkQ2hjGNTA+ARxwgn0eQJLNPAXsb5Qz10hXFRPbw=; b=UQQWKX5vWxLdqaXgKB7ZAeyJU08lvXRYtKfkSVgNvfI+Srz5Agx/XZ1AApCOB056fo rzD2U94tJTtI0q3H6WVm3zYgg0sIybTsVlGQk0pjDpJVcYZf/wa7MAOP2HHHoWLa/1bQ CfFeN//X8JhdhB8518ppTfzdnQ9MII2haU0mSxpi/K5KhNdxggML6FCcji/kz1pgUftZ Cx3r5T5ATT9QT2Rhk8DpnFLix3R3MFxG9BD697XLXfz03S878DSpkSDpn5QlT07RhM9j JsKBpmGGIys7y6UGkipAnrj+rFWvzyjspEGFZ3pWnIEZP/jXgmjJRlKZRXYPVwe3/B86 a0Iw== 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=NaZjkQ2hjGNTA+ARxwgn0eQJLNPAXsb5Qz10hXFRPbw=; b=PYbpGuPHqz7JeG7991AxZwVc6c9Fh8ICgEqhVd25NPxbT77ICEJ9fw14R1D4XjjwAX 6Qc+MsPsktTZyWOetw78ekcq1vLaYpB9LGnJJ/UuvUF2XQavupr1TKjN2UHGf0ZlwjsX ah8+UKEeVu2b+NHuPm+PohJ7Igv6XToGudKDHBD3R0P0MJPpBRsasFkIvGl+abqgX5J1 CMWeTb5L4wHjp2odNPOatoJcn/I/oIhzexjsVHCghU1JwP2FpLRUGDU0IrVjaue8JpmE 14kX/xOmGhSmbM4hD5v3gOTY4A4l/eXectBfXgCQimvKcl9f1jV0h6/SJQ7QYlGewzud 7jxQ== 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=NaZjkQ2hjGNTA+ARxwgn0eQJLNPAXsb5Qz10hXFRPbw=; b=pllGJfF7iXjdmL+sWcjLT9lkX0IWQkNQdrZtce+DbWlW3WmLZDpZF33fuGLzhbwHKk ZUt3NQ2LsvBWD6OBWqt98nHA8dSB0KRKcVWiX8i9eblR5hLJ830M0mpYD8KSt/QSoqoP J6ZX1gk7lyp0ph38mjfVTraJTUq+FUMi3P8z3nSvifVmZaHRE/16PElAwQv3nUlpeoDi XN/R8KpaumurcolRJPXouStXjOCdGyop1AIQhf2klwxnPkNG8t0M/wuKQKuL5CpJ1bpg GIxearDGWlx/41e38DEDjN8yNRheOYpaGJdvaNlIgoitsUeVlN3QVslizbWUrNbSjfoM T68w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E0m5e0P1H2QRNz6wNfs8eb0FRQHx5iOWKmlwHO4WdkvzUcwmBXd Hty4duOIE5WYsELs7RQCE9o= X-Google-Smtp-Source: ADUXVKKP27ezHPuRviKaDwBOk1Hi6L50LsnBlcH3jvI+GOSqiGq3bIaflP3i+KGsYCcvsK1bPNqA2Q== X-Received: by 2002:aca:d60f:: with SMTP id n15-v6mr876816oig.6.1529474573477; Tue, 19 Jun 2018 23:02:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:30d8:: with SMTP id w207-v6ls675143oiw.5.gmail; Tue, 19 Jun 2018 23:02:53 -0700 (PDT) X-Received: by 2002:aca:a883:: with SMTP id r125-v6mr862863oie.7.1529474572752; Tue, 19 Jun 2018 23:02:52 -0700 (PDT) Date: Tue, 19 Jun 2018 23:02:52 -0700 (PDT) From: xieyuheng To: Homotopy Type Theory Message-Id: In-Reply-To: <9b68a44e-7c9c-451b-8aab-a7a4c972ba6c@googlegroups.com> References: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> <9b68a44e-7c9c-451b-8aab-a7a4c972ba6c@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_22839_664623273.1529474572208" 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_22839_664623273.1529474572208 Content-Type: multipart/alternative; boundary="----=_Part_22840_1605758203.1529474572209" ------=_Part_22840_1605758203.1529474572209 Content-Type: text/plain; charset="UTF-8" Oh! I mistakenly thought a polymorphism is a morphism in a polycategory, only later realized that polymorphism is the term from programming language. if polycategory is unrelated, I can try to develop a generalized theory based on my simple idea above. I read through the page << Categorical models of dependent types >> on nLab. it seems unsorted. and the categorical model for dependent type system is a unsolved problem. ------ xieyuheng On Wednesday, June 20, 2018 at 2:59:38 AM UTC+8, Matt Oliveri wrote: > > 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_22840_1605758203.1529474572209 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Oh! I mistakenly thought a polymorphism is a morphism in a= polycategory,
only later realized that polymorphism is the term from pr= ogramming language.

if polycategory is unrelated,
I can try to de= velop a generalized theory based on my simple idea above.

I read thr= ough the page << Categorical models of dependent types >> on nL= ab.
it seems unsorted.
and the categorical model for dependent type s= ystem is a unsolved problem.

------
xieyuheng


On Wedne= sday, June 20, 2018 at 2:59:38 AM UTC+8, Matt Oliveri wrote:
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 agai= n :)

So polycategories had to do with the cu= t rule, which is not what your examples are doing. I don't think you ne= ed to worry about polycategories. I don't think there's much connec= tion between polycategories and polymorphism, other than the prefix "p= oly".

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, oth= erwise I would've said so earlier.) Thinking of the underlying monomorp= hic (non-polymorphic) stack types as contexts, I figure the approach should= generalize to dependent contexts, with the operations being polymorphic su= bstitutions between dependent contexts.

So I think the ingredients y= ou want are some dependent generalization of row polymorphism, and some cat= egorical approach to interpreting the underlying monomorphic contexts and s= ubstitutions, like contextual categories.

There are a lot of approac= hes 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/nl= ab/show/categorical+model+of+dependent+types
<= /blockquote>

--
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_22840_1605758203.1529474572209-- ------=_Part_22839_664623273.1529474572208--