Iterating families of maps over a map

[fredrik-bakke]

Adds a module about iterating families of maps over a map, and does some refactoring for inverse sequential diagrams.

[fredrik-bakke]

@VojtechStep I couldn't help but notice that this sort of formalization would probably help streamline reasoning about shifts of sequential diagrams as you do in synthetic-homotopy-theory.shifts-sequential-diagrams. Entries such as shift-sequential-diagram and shift-cocone-sequential-diagram can be replaced with iterate and iterate-dependent without issue, but shift-hom-sequential-diagram seems to need iterated doubly-dependent functions.

[VojtechStep]

Looks like shifts should be definable with iterate(-dependent), and unshifts with iterate(-dependent)', though I'm not sure how it affects reasoning about them.

[EgbertRijke]

This is a great pull request, but I'd like to think about the naming some more:

Could we express this concept more accurately by saying that we are iterating families of maps over a map? Of course, there dependency is necessary to express this concept, but to me iterating a dependent function suggest that a general dependent function is iterated somehow. If we say that we're iterating a family of maps over a map, perhaps that is more easily interpreted correctly by someone who doesn't already know what concept is implemented here.

[fredrik-bakke]

Right, I agree this is more accurate. Thank you for the feedback! Do you think the module name iterating-families-of-maps is sufficiently precise, or is it too easy to confuse with iterated-families-of-maps?

[fredrik-bakke]

Looks like shifts should be definable with iterate(-dependent), and unshifts with iterate(-dependent)', though I'm not sure how it affects reasoning about them.

Well, for instance, you can observe that the lemma reassociate-iterate-family-of-maps could be used to reassociate instead of repeating this proof for every construction.

EDIT: Not that this is done anywhere. It's a merely hypothetical use case

[fredrik-bakke]

Right, I agree this is more accurate. Thank you for the feedback! Do you think the module name iterating-families-of-maps is sufficiently precise, or is it too easy to confuse with iterated-families-of-maps?

@EgbertRijke