From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGPPLV76EPRBC7TV7MQKGQE2FMBLGA@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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-io0-x23d.google.com (mail-io0-x23d.google.com [IPv6:2607:f8b0:4001:c06::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6611ce0a for ; Thu, 21 Jun 2018 19:16:28 +0000 (UTC) Received: by mail-io0-x23d.google.com with SMTP id g20-v6sf3332337ioc.4 for ; Thu, 21 Jun 2018 12:16:28 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1529608587; cv=pass; d=google.com; s=arc-20160816; b=ghQlmOJv9VQwfbBDlqBTkbXP4QsJYuLd6N6eNvu09TNauN8sHX86zCna8uzFX2kC/A hRxSpnQwb8DKUCEuzTcfVxs86HMxdJwcOtKV1AX6aaqMJjhdh7RaV6KGLEksXNwkgJ5V GJzwhRIqHkH8UJSDii5zCLedDMSS1ch9+rtH+cXG8SW+jEmfbk7gPC/U4HA4PGZMEQ+A Yo9kGnEv5WZ+kTYe/nDMjP2UWQXWc1H0KNumMaFVDXODCAza9mF31KvRYBoS1vv+ot2a 5QvamEAQ+3SHyO81k+d50mqUbR8a5HLmu6hiLqj+AkVqjelH3BbcgVVUNBW8kzecLZm1 lNbA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from:references :in-reply-to:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature:dkim-signature :arc-authentication-results; bh=pK2O13H1eZSRpQZsO192pwB+CLmqK2gnKiX5t01LZIw=; b=pCcvIG53Cby3De/mLD3t3+ZDgvTvqsAcFj9vKc9/0I04A/XPLT/TCKMCPXIKrk7dvj kFRajcIz8dpkrg3GSHqgBQwen/6bJrKTh7oRpbBK/kfS6JgOdgeLH41ogI8Z6nK/pPwz 4KangE1aqGYSBww1atQEUyqljGGnJ7wiAhILvVZj2GY7hyFfEGYwB0VHaQCDM762tbQA QEwYcAPZUZDSnwS9ZyiGSxv7PrPVGGjolNAuIWLyW5Pj9gKErwRqaa5uCNiy4davUqyt AtLMKeHcjHMU/6oMZxq332EbDLtZ9M2gdJf0CLUdGPhQcZxrQv4EBKo6u3fCCaQRbzic 3eqQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VQ3vU0Dv; spf=pass (google.com: domain of xyheme@gmail.com designates 2607:f8b0:4003:c06::234 as permitted sender) smtp.mailfrom=xyheme@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:in-reply-to:references:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=pK2O13H1eZSRpQZsO192pwB+CLmqK2gnKiX5t01LZIw=; b=V05y3hOlqF3oMHlVIZ4iZiOTkynIHCQBd4Zh6O57k4z92caVreRW/Pplzi1nYXps5M iIpcvTt4Q/15QHpoIHFaFLmPEYqgbevd1rchTnvBT7LI4NxX4AziBFETCHRs/czCqFXM IBAoIHgSEkrppbD4bqjWPYu9kXnbQBzL2Q5i3uqDcFwU8VsfYkMbKZUIbWQ2Vs4+5UUZ cAIDJcat/x33a/WBgdevQmoJXF1aAJO7ajSrwtA+vsAuvQUR851zhlCBPgXM2MBmMstk nj0WAYXDzHYl9Loet3dcKjh5iIuPQaqZoMHDh9kqr4kZH5rbEVnWLk6YIjgPYSEVMMCz s3Uw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=pK2O13H1eZSRpQZsO192pwB+CLmqK2gnKiX5t01LZIw=; b=V8OrGNGsXPTgrpXwvE7U2DuZSUZ77XZQmkajWw//puawzFtKlDV0ySnTXB//KY/W/6 RwX9TgQvINpeMOKFXPMqK8lN86LGTWCFf10JBJwISQT0BOGlkqJsLBk1aPe+yHGbIwS+ OZGatiRPowrfsdDvBpNfq6C9fe97VA2KZgM5vNSK+pP0/skOncXKlvg0AuKV1X35qk0W faq9gASkeQ72cotJ81vOMMsWvVPVTzbFOp20Nep3ig2kaC5imHGcdlj9lAxoNO1G0n8e 0050V3fQgHc0zKrUWOykEN+FozI9e+8OYltqezTRgwE81uEKJou8z0TpS3xd1y+rg+pX /zaA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:in-reply-to:references:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=pK2O13H1eZSRpQZsO192pwB+CLmqK2gnKiX5t01LZIw=; b=qOGoAn9f4xXP6aJn+THRU2yQj+cE92ABsdrdSoDRGilluk2afeZDkhsaC0V4ke5uB+ 7LscoDeVa0diT5etVVM1ucchABBZ+MD6iGvU0b79q3tq0zTD29RfTZ0vv3g06Hgvykfn i9dLRAvvDPj7XK9Cj8fZkrN+J9t4J2U/hF1ya6N4B/pd3WWR4Y4iHl/89k8pxvud0fJ6 Igbbmvhdvc/lt+VXPIyIVKVse8WedKYsFkOtZcderfm9zgTtNZ6CzciEEdDxv6TI3Mmf 8Q1VBHd6YovLq3yLm8J70dHFCwpWIeSNEGIQcfDsVxD3nYTMBT2OY/Sv+mNqqeA4Mwr+ gAtA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E17juFbftLRt4vgcmdJx+JtG4efUItcf5gXmY8sKDqtR3Ip/rLJ sB5EwOyGNAj5r5k1VI7leBw= X-Google-Smtp-Source: ADUXVKLAQpKdkcHA7M9LAJpI99PIk5fXWqFkDVJgI76JHAZOBgReTetpzjTkJPv0DIyDXNc3KMPpaQ== X-Received: by 2002:a6b:9645:: with SMTP id y66-v6mr112116iod.0.1529608587173; Thu, 21 Jun 2018 12:16:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:520e:: with SMTP id g14-v6ls921854iob.18.gmail; Thu, 21 Jun 2018 12:16:26 -0700 (PDT) X-Received: by 2002:a5e:870d:: with SMTP id y13-v6mr2391226ioj.1.1529608586834; Thu, 21 Jun 2018 12:16:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1529608586; cv=none; d=google.com; s=arc-20160816; b=RpH7ZVYrpHr9nGTsdEPOOEgFbbI44rFfdBYZUZlkGl5j3DWQ1UNo+lINunYDvBXN0Q KEPA0KOvpne73u6l2mFWhRXqBklG3S0MZ+gdpo/Twj2WaSWyRkaEx4T9uxIMYK6a4s2Q cEEj8bwOaXKsKUbH/AjTbqw2i+B+KeLBvAXk094x5LNnNwrYXIefUlSPoQw5cl2QdvDN lqvjf/90lV+LJxeHTMoNsEErUsdZFxorA+rhxYnGq7kUsnDfq0LGwP0mBccEEyqar1hL DJpgLOqvm4EtMTS9zJNWAgASgAsD5JNqxjALGoBOrEe/x61ix8HeJ/PU0+uDdnQoQh33 ZFTQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=WUjaIeA2B0I3USJju6sMGLEQ+cAbA6hN0qu8p3sWlas=; b=zWc9DWLASQNlDHYNTG/gI9PzhEcS0U7mi8cnMgSm+a288bIz69kIqB7uMd3avi5yVH 6VEQsF5v4dKnWL4wHMYL0PeG8GFPZebUxfaBdT6LST2+qE7rM1u78RJILzcGnufOQ1KI iKQEI1EyH/X/9BtvRBSPa+2mz86e+LTi7uF3r6u3gO4aen7rSIttXFs0HgxpT2w5KNd6 /b6PCuriF12VaUyEHNmxtt96qJDLC//AoOrOCyKxLC5OcssTuGnRhxQw1amaQk8aqW18 uSM3ydbV6gDo7+B5j0OhVoI21zJiSNLxfqQFcO+7YY3+/JYIB//4BTIddRVO5BCl5avI v5ig== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VQ3vU0Dv; spf=pass (google.com: domain of xyheme@gmail.com designates 2607:f8b0:4003:c06::234 as permitted sender) smtp.mailfrom=xyheme@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi0-x234.google.com (mail-oi0-x234.google.com. [2607:f8b0:4003:c06::234]) by gmr-mx.google.com with ESMTPS id o70-v6si119766ito.1.2018.06.21.12.16.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 21 Jun 2018 12:16:26 -0700 (PDT) Received-SPF: pass (google.com: domain of xyheme@gmail.com designates 2607:f8b0:4003:c06::234 as permitted sender) client-ip=2607:f8b0:4003:c06::234; Received: by mail-oi0-x234.google.com with SMTP id c128-v6so3927798oig.11 for ; Thu, 21 Jun 2018 12:16:26 -0700 (PDT) X-Received: by 2002:aca:4bd7:: with SMTP id y206-v6mr14357669oia.181.1529608586466; Thu, 21 Jun 2018 12:16:26 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a4a:9c45:0:0:0:0:0 with HTTP; Thu, 21 Jun 2018 12:16:26 -0700 (PDT) In-Reply-To: References: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> <9b68a44e-7c9c-451b-8aab-a7a4c972ba6c@googlegroups.com> From: xieyuheng Date: Fri, 22 Jun 2018 03:16:26 +0800 Message-ID: Subject: Re: [HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ? To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: xyheme@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VQ3vU0Dv; spf=pass (google.com: domain of xyheme@gmail.com designates 2607:f8b0:4003:c06::234 as permitted sender) smtp.mailfrom=xyheme@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , I just wrote something on this tpoic :: https://xieyuheng.github.io/output/dependent-category.html (if you use github) welcome to leave message by open new issue on the repo :: https://github.com/xieyuheng/xieyuheng.github.io/issues ------ xieyuheng 2018-06-20 14:02 GMT+08:00, xieyuheng : > 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. > -- 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.