Path-cosplit maps

[fredrik-bakke]

A (mere) k-path-cosplit map is defined inductively

• A (mere) -2-path-cosplit map is a map that is (merely) a retract
• A (mere) k+1-path-cosplit map is a map whose action on identifications is (merely) k-path-cosplit.

We show

• Mere k-path-cosplitting is a property
• k-truncated maps are k-path-cosplit
• (merely) k-path-cosplit maps are (merely) k+1-path-cosplit
• types that map into k-truncated types via (mere) k-path-cosplit maps are k-truncated
• (mere) k-path-cosplit maps into k-truncated types are k-truncated.

[fredrik-bakke]

I should introduce path-cosplit maps and mere path-cosplit maps as separate notions. I'll leave this PR as a draft until I do.

EDIT: done.

[EgbertRijke]

Nice! Just a pointer from the injective maps file to these would be nice I think, so that people can be more easily aware of these concepts.

[fredrik-bakke]

Thanks for the swift review! Hopefully, this concept comes in useful. I don't think I've heard of a concept such as this one before, but it seems like it should be possible to do some homotopy group computations with it.