Added dependent analogue of [transport_paths_FlFr].
Added eta-rule for Suspension.
Showed that truncatedness is equivalent to maps from spheres being null-homotopic.