proposition: Theorem iscontrGuidedHomotopy {Y} (T:Torsor ℤ) (f:T->Y) (s:target_paths f) : iscontr (GuidedHomotopy s).
proof: Proof. intros. apply (squash_to_prop (torsor_nonempty T)). { apply isapropiscontr. } intro t0. apply ( iscontrweqb (Y := ∑ y:Y, y = f t0)). { apply weqfibtototal; intro y. exact (ℤTorsorRecursion_weq (λ t, weq_pathscomp0r _ _) t0). } apply iscontrcoconustot. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.MoreEquivalences UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.GroupAction UniMath.NumberSystems.Integers