fact: Definition target_paths {Y} (f:ℕ->Y) := ∏ n, f n=f(S n).
imports: UniMath.Foundations.All UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA