proposition: Theorem iscontrGuidedHomotopy {Y} {f:ℕ->Y} (s:target_paths f) : iscontr (GuidedHomotopy f s).
proof: Proof. intros. unfold GuidedHomotopy, nullHomotopyFrom. refine (@iscontrweqb _ (∑ y, y=f 0) _ _). { apply weqfibtototal. intro y. exact (Nat.Uniqueness.hNatRecursion_weq (λ n, y = f n) (λ n hn, hn @ s n)). } { apply iscontrcoconustot. } Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA