fact: Definition gHomotopy {Y} (f:ℕ->Y) (s:target_paths f) := fun y:Y => ∑ (h:nullHomotopyFrom f y), ∏ n, h(S n) = h n @ s n.
imports: UniMath.Foundations.All UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA