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

[Matt Oliveri <atmacen@gmail.com>]

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

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: 2084 bytes --]