proposition: Lemma loop_compute t : castTorsor (!circle_loop) t = one + t.
proof: Proof. intros. unfold circle_loop. rewrite pathsinv0inv0. exact (loopsBG_comp_2 _ one t @ commax _ t one). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.NumberSystems.Integers UniMath.SyntheticHomotopyTheory.AffineLine UniMath.Algebra.GroupAction UniMath.MoreFoundations.MoreEquivalences