proposition: Lemma circle_map_check_paths' {Y} (f:circle->Y) : circle_map (maponpaths f circle_loop) = f .
proof: Proof. intros. apply funextsec. simple refine (circle_map' _ _ _). { reflexivity. } { set (y := f (basepoint circle)). set (l := maponpaths f circle_loop). set (P := λ T : underlyingType circle, circle_map _ T = f T). apply transport_fun_path. rewrite pathscomp0rid. change (idpath y @ maponpaths f circle_loop) with (maponpaths f circle_loop). exact (! circle_map_check_paths l). } 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