Dependent path composition in ordinary higher category theory

[Noah Snyder]

Section 2.3 of the book introduces "dependent paths" (which are paths in a fibration "lying over" a path in the base) and "dependent path composition" which composes such dependent paths when that makes sense.  I'm working on a paper that's not about HoTT but where "dependent path composition" plays an important role.  The problem I'm running into is that I don't know what dependent path composition is called in "standard" mathematics.  Does anyone know if this has another name in higher category theory?  (Naturally, we'll include a remark mentioning the HoTT way of thinking about this (since it's how I think about it!), but I think that won't be illuminating to most of our target audience.)

The simplest example of what I have in mind here is if C is a category and F is an endofunctor and c is an F-algebra (i.e. we have endowed c with a chosen map f: F(c) --> c) then c is also an F^n-algebra by taking the "nth power of f" which actually means f \circ F(f) \circ F^2(f) \circ ... \circ F^{n-1}(f).  In particular, I think this example illustrates that you can talk about "dependent k-morphisms" and their compositions without requiring anything in sight to be a (higher) groupoid.

My best guess is that the right setting might be "indexed (higher) categories"?

Best,

Noah

[Noah Snyder]

Mike pointed out that I didn't explain how my example is a special case of dependent path composition.  A type family over S^1 is a higher groupoid together with an (invertible) endofunctor F.  A path over loop is an algebra for that endofunctor (where the map is an iso).  If you dependent path compose it with itself n times you get a path over loop^n, i.e. an algebra for F^n.  Best,

Noah

[Michael Shulman]

Yes, I think probably you want indexed categories, incarnated as
fibrations. You can then remove the invertibility too: if C is the
1-object category corresponding to the monoid of natural numbers, then
an opfibration over C is a category equipped with an endofunctor, an
endomorphism over the generating morphism of C is an algebra for that
endofunctor, and its n-fold composition with itself is the
corresponding algebra for F^n.

> --
> 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 HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg5mstbw3Ujjfu%2BkMfgW7_7y7raxbWV_yh-2phB2ynwb8g%40mail.gmail.com.