proposition: Theorem circle_induction : CircleInduction circle pt loop.
proof: Proof. apply CircleInductionEquiv. unfold CircleInduction'. intros A a p. set (f := c p). exists f. set (h := c_tilde p pt); fold f in h. set (h0 := h pt_0). set (e := Δ (cp s_compute_0 h0)). exists e. assert (q := c_hat p pt); fold h in q. set (s0 := s pt_0); unfold pt_0 in s0. set (s1 := s pt_1); unfold pt_1 in s1. set (one' := transportf elem loop pt_0); fold pt in one'. assert (r := apd_comparison p loop pt_0). fold pt h h0 f one' in r; unfold pt_0 in r. apply (pr2 (composePathPathOverRotate _ _ _)). rewrite composePathPathOverPath. refine (r @ _); clear r. assert (ss : one' = pt_1). { unfold one'. refine (castTorsor_transportf (invmap torsor_univalence _) _ @ _). apply torsor_univalence_inv_comp_eval. } unfold pt_1 in ss. set (s0sm := λ m:ℤ¹, ! s0 @ s m). assert (b : cp (ε' loop 0) (h0^-1 * h one') = cp (ε'' 0) (h0^-1 * h (1 + pt_0))). { intermediate_path (cp (ε'' 0) (cp (maponpaths s0sm ss) (h0^-1 * h one'))). - intermediate_path (cp (maponpaths s0sm ss @ ε'' 0) (h0^-1 * h one')). + apply cp_irrelevance_circle. + apply cp_pathscomp0. - apply maponpaths. exact (cp_in_family _ (λ m, h0^-1 * h m)). } refine (b @ _); clear s0sm b. unfold pt_0. rewrite (q 0). fold h0. clear q ss one'. set (α0 := invrot' (s_compute_0 : s0 = ! idpath _)). transparent assert (α : (!s0 @ s1 = idpath pt @ (loop @ s0))). { exact (apstar α0 (!ε pt_0)). } transparent assert (β : (idpath pt @ (loop @ s0) = idpath pt @ (loop @ idpath pt))). { exact (apstar (idpath _) (apstar (idpath loop) s_compute_0)). } transparent assert (γ : (idpath pt @ (loop @ idpath pt) = idpath pt @ loop)). { exact (apstar (idpath _) (pathscomp0rid _)). } intermediate_path (cp (α@β@γ) (h0^-1 * cp (ε pt_0) (p * h0))). { apply cp_irrelevance_circle. } rewrite cp_pathscomp0. unfold α. rewrite cp_apstar. rewrite inverse_cp_p. rewrite cp_pathscomp0. unfold β. rewrite cp_apstar. rewrite cp_idpath. unfold γ. rewrite cp_apstar. rewrite cp_idpath. rewrite cp_apstar. change (cp s_compute_0 h0) with (∇ e). change (cp (idpath loop) p) with p. rewrite composePathOverPath_compute, composePathPathOver_compute. intermediate_path (cp (pathscomp0rid loop) (cp α0 (h0^-1) * p * ∇ e)). { rewrite cp_left. apply (maponpaths (cp (pathscomp0rid loop))). exact (assocPathOver (cp α0 (h0^-1)) p (cp s_compute_0 h0)). } rewrite cp_apstar'; fold s0. unfold α0. rewrite invrotrot'. change (cp s_compute_0 h0) with (∇ e). rewrite inversePathOverIdpath'. reflexivity. 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