fact: Definition iscontrGuidedHomotopy_comp_1 {Y} : let T := trivialTorsor ℤ in let t0 := 0 : T in ∏ (f:T->Y) (s:target_paths f), GH_point (iscontrpr1 (iscontrGuidedHomotopy s)) = f t0.
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