proposition: Lemma CircleInductionEquiv (circle : Type) (pt : circle) (loop : pt = pt) : CircleInduction circle pt loop ≃ CircleInduction' circle pt loop.
proof: Proof. unfold CircleInduction', CircleInduction. apply weqonsecfibers; intro X. apply weqonsecfibers; intro x. apply weqonsecfibers; intro p. apply weqfibtototal; intro f. intermediate_weq (∑ r : f pt = x, !r ⟤ apd f loop = p ⟥ !r). - apply weqfibtototal; intro r. intermediate_weq (PathOver (Y := λ t:X pt, PathOver loop t t) (!r) p (apd f loop)). + apply inversePathOverWeq. + induction r. cbn. apply weqpathsinv0. - exact (weqfp (make_weq _ (isweqpathsinv0 _ _)) _). 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