Iterating dependent functions

[fredrik-bakke]

Adds a module about iterating dependent functions, 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.