Composing finite number of morphisms?

Stream: Is there code for X?

[Chiyu Zhou]

Hello, I'm a math undergraduate and I'm now working on proving van kampen theorem, groupoid version. In some part of the proof I need to cut a path p : path a zinto finite pieces p1 : path a b, p2 : path b c... pn : path y z, map these pieces into morphisms (endpoints specified, so types are different) m1 : a -> b, m2: b -> c ... mn : y -> z in a groupoid, and then compose them to get a single morphism a->z . Now I've already managed to store the morphisms m1 : a -> b, m2: b -> c ... mn : y -> z in d_array, but lfold doesn't work because it requires the output to be all of the same type. What shall I do now? Perhaps I shall do some sort of induction?

[Chiyu Zhou]

There's also a concern that the endpoints may not be definitionally equal. i.e. I may need to compose m1 : a - >b, m2 : b' ->c but with a proof of b = b'. :pensive:

[Junyan Xu]

I think docs#category_theory.compose_path is what you are looking for; you should use docs#quiver.path instead of d_array. I don't know how your endpoints could be non-def-eq, but in category theory the way to compose morphisms with an equality proof at the endpoints is to insert a docs#category.eq_to_hom.

[Junyan Xu]

I'm wondering whether we should make a docs#quiver instance on every topological space with hom x y := path x y.

[Andrew Yang]

We already have a quiver instance for all preorders IIRC. So that might give diamonds on ordered topological spaces.