proposition: Lemma s_compute_0 : s pt_0 = idpath pt.
proof: Proof. intermediate_path (invmap torsor_univalence (idActionIso ℤ¹)). - change (s pt_0) with (invmap torsor_univalence (triviality_isomorphism ℤ¹ 0)). apply maponpaths. exact (triviality_isomorphism_compute ℤ). - apply torsor_univalence_id. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Equivalences UniMath.MoreFoundations.PathsOver UniMath.Algebra.Monoids UniMath.SyntheticHomotopyTheory.AffineLine UniMath.NumberSystems.Integers UniMath.Algebra.BinaryOperations UniMath.Algebra.GroupAction UniMath.Algebra.Groups