[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: 4315 bytes --]

thank you Matt Oliveri.

the substitutions you used above explains my examples perfectly.
I also found a bug in my second examples :

f   : (A, t1, t2) -> (A, t, t3, t4)
g   : (B, t3, t4) -> (B, t6, t7)

(unify)
B = (A, t)

f   : (A, t1, t2) -> (A, t, t3, t4)
g   : (A, t, t3, t4) -> (A, t, t6, t7)

f;g : (A, t1, t2) -> (A, t, t6, t7)

(shorten)
f;g : (t1, t2) -> (t, t6, t7)

(but I mistakenly wrote)
f;g : (t, t1, t2) -> (t, t6, t7)

---

I will learn more about polycategory and polymorphic,
and try to use them to explain dependent type system.

thank you again :)

------

xieyuheng


On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Oliveri wrote:
>
> Hi, Xieyuheng.
>
> On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote:
>>
>> is there a categorical construction to generalize arrow composition,
>> by allowing domain and codomain to be refined (or changed) by the
>> composition ?
>>
>> this construction would be useful for
>> forming theoretical background of dependent type system.
>>
>> for example, compose two functions
>> f : (A x -> B y)
>> g : (B n -> C z)
>> will give us a function of type (A n -> C z)
>>
>
> I can't figure out what rule you're using to get that type. If n unifies 
> with y, how did x become n also? That's what I'm guessing you're trying.
>
>
>> another example would be the following generalized composition in 
>> cartesian closed category :
>>         f   : (t1, t2) -> (t3, t4)
>>         g   : (t, t3, t4) -> (t6, t7)
>>         f;g : (t, t1, t2) -> (t6, t7)
>> and
>>         f   : (t1, t2) -> (t, t3, t4)
>>         g   : (t3, t4) -> (t6, t7)
>>         f;g : (t, t1, t2) -> (t, t6, t7)
>> this can be called `cut`
>> because it looks like gentzen's cut rule in sequent calculus,
>> and it can be used to provide semantic
>> for a stack based concatenative programming language.
>>
>
> This looks more like a combination of composition and tensoring, in a 
> monoidal category. Based on some stuff in a blog post (
> https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivaria.html), 
> the cut rule is instead composition in a polycategory, and you can only cut 
> out one type at a time.
>
> I'm thinking the first "generalized composition" could be explained thus:
> f only looks at the top two stack elements, and replaces them with three 
> others. But the stack generally has additional elements, which I'll 
> abstract away as Γ:
> f  :  (Γ, t1, t2) -> (Γ, t3, t4)
>
> g has a similar story, but we use a different stack/context variable to 
> avoid accidental constraints:
> g  :  (Δ, t, t3, t4) -> (Δ, t6, t7)
>
> To compose these, we need (Γ, t3, t4) to unify with (Δ, t, t3, t4), so (Γ 
> := Δ, t), and
> f;g  :  (Δ, t, t1, t2) -> (Δ, t6, t7)
> which we shorten to (t, t1, t2) -> (t6, t7).
>
> So your composable operators seem to be substitutions (morphisms between 
> contexts) that are polymorphic in most of the context. All but a finite 
> chunk all the way on the right. Composition would presumably be composition 
> of substitutions, after instantiating them with the principal unifier.
>
> For simply-typed systems, contexts and substitutions can be modeled in a 
> monoidal category, which includes cartesian closed categories. For 
> dependent type systems, other kinds of categories are used, like contextual 
> categories and categories with families; hopefully what you want is still 
> instantiation and composition of this new kind of substitution.
>
> I'm not an expert on the kinds of categorical structures involved, but 
> hopefully polymorphic substitutions is a good way of thinking about what 
> you're doing, which connects it with categorical models.
>
> Beware that with dependent types, there generally are not principal 
> unifiers, due to binding operators appearing in types. But concatenative 
> people don't seem to like binders, so maybe you dodged the bullet.
>

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