proposition: Lemma CircleRecursionEquiv (circle : Type) (pt : circle) (loop : pt = pt) : CircleRecursion circle pt loop ≃ CircleRecursion' circle pt loop.
proof: Proof. unfold CircleRecursion', CircleRecursion. apply weqonsecfibers; intro X. apply weqonsecfibers; intro x. apply weqonsecfibers; intro p. apply weqfibtototal; intro f. intermediate_weq (∑ r : f pt = x, maponpaths f loop @ r = r @ p). - apply weqfibtototal; intro r. apply eqweqmap. induction r. cbn. apply (maponpaths (λ k, k=p)). rewrite pathscomp0rid. reflexivity. - intermediate_weq (∑ r : f pt = x, (!r) @ maponpaths f loop = p @ (!r)). + apply weqfibtototal; intro r. induction r. cbn. rewrite 2 pathscomp0rid. apply idweq. + exact (weqfp (make_weq _ (isweqpathsinv0 (f pt) x)) _). 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