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