[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng <xyheme@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2238 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 3385 bytes --]