Dependent universal property of suspensions

[morphismz]

This pr contains further development of the dependent universal property of suspesions. This includes:

• proof that suspensions have the dependent universal property, found in dependent-up-suspension
• a characterization of homotopies out of suspensions, found in equiv-htpy-function-out-of-suspension-htpy
• necessary lemmas for the above two

This completes one of the tasks in #702

NOTE: I will rename variables, since I wrote this before reciving the feedback on long variable names. I'll do that later today or tommorow.

[EgbertRijke]

Your code is starting to look very good!