proposition: Lemma CircleInduction_isaprop (circle : Type) (pt : circle) (loop : pt = pt) : isaprop (CircleInduction circle pt loop).
proof: Proof. Abort. Lemma CircleInductionToRecursion' (circle : Type) (pt : circle) (loop : pt = pt) : CircleInduction' circle pt loop -> CircleRecursion' circle pt loop. Proof. intros I. unfold CircleRecursion'. intros X x p. set (w := I (λ _, X) x (PathOverConstant_map1 _ p)). simpl in w. exists (pr1 w). exists (pr12 w). refine (_ @ maponpaths PathOverConstant_map2 (pr22 w) @ _). { apply pathsinv0. refine (PathOverConstant_map2_eq2 _ _ @ _). apply maponpaths. apply PathOverConstant_map2_apd. } { refine (PathOverConstant_map2_eq1 _ _ @ _). apply (maponpaths (λ t, t @ _)). apply PathOverConstant_map1_map2. } 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